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


1 edited


  • Deliverables/addenda/letter.tex

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