Changeset 804 for Deliverables/addenda/letter.tex

Timestamp:

May 13, 2011, 6:18:41 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/addenda/letter.tex (modified) (1 diff)

Deliverables/addenda/letter.tex

@@ -123 +123 @@
  b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
 
-
+ We will stop and spend some time on the proposed comparison. Nevertheless,
+ we remark here a few points that are important to put the project in our
+ perspective.
+ \begin{enumerate}
+  \item CompCert proofs are not open source. All commercial uses are prohibited
+   by the licence. One of the strong points of the project proposal was to
+   obtain a fully open source verified compiler. This does not allow us to
+   re-use at all CompCert proofs (the intermediate languages are instead put
+   under GPL). Of course, we could re-discuss the open source project
+   requirement, but for reasons I am not listing here we do champion open
+   source, in particular for software developed using public money.
+  \item CompCert is surely part of the state of the art in compiler
+   certification. The proofs are very well organized and the authors are
+   trying to maximise simplicity and reusal. Nevertheless, some important design
+   decisions have been taken from the very beginning and have not been
+   questioned estensively. Among them, the use of non executable semantics
+   for intermediate languages and the use of non dependent types for the code.
+   From our point of view, the CerCo project is first of all a project in
+   compiler certification. Therefore, we are interested in exploring the
+   design space for compiler certification. For this reason, already in the
+   project proposal, we decided to start from different assumptions. In
+   particular, we will favour dependent types and executable semantics.
+   We are not claiming in advance that we will obtain better results than
+   CompCert: what we are claiming is the interest in comparing large scale
+   solutions based on different techniques. We also note that the one used
+   in CompCert are very reasonable because of the choice of Coq that,
+   traditionally, has favoured the use of non executable, inductive
+   specification over executable ones.
+  \item If we decide to depart from the choices we made in the project
+   proposal and reuse CompCert proofs, this does not imply automatically that
+   it is decisively better for us to switch from Matita to Coq. Indeed, the
+   effort of just porting verbatim the proofs from Coq to Matita is very small.
+   Indeed, as said before, our interest is in changing the proofs themselves.
+   We should therefore decide if it would be easier to port verbatim the
+   proofs to Matita or if it would be simpler to port the deliverables already
+   done in Matita to Coq. Since we have already used some features of Matita
+   not available in Coq and since we have more control over Matita, it is not
+   obvious a priori what solution would be lighter for us.
+  \item It is clear that one partner is interested in promoting the use of
+   Matita. We think that more competition in the domain of interactive theorem
+   proving will be rewarding for the community as a whole. Indeed, Coq saw
+   many interesting improvements in the period when it co-existed with Lego,
+   an alternative implementation of the same calculus. Moreover, some ideas
+   developed for Matita have already been ported to Coq itself, and the two
+   systems show alternative solutions for similar problems that are still
+   under comparison (e.g. Matita's unification hints vs Coq type classes).
+   One of the major struggles of EU funded research, and FET in particular,
+   is the balance between innovation and stability. While the promotion and
+   improvement of Matita is not a major goal for the project, we believe that
+   it will provide some good side outcomes, as it happened in the past when
+   Matita was used for some major formalizations and new techniques were
+   develop recurring problems. This would be hardly possible using Coq since
+   nobody in the CerCo team is part of the Coq developing team and has enough
+   expertise to quickly modify such a large system as Coq.
+ \end{enumerate}
 
 \end{enumerate}