Changeset 804
 Timestamp:
 May 13, 2011, 6:18:41 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/addenda/letter.tex
r803 r804 123 123 b) port D3.1 and D4.1 to Coq and reuse the CompCert proofs. 124 124 125 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 reuse at all CompCert proofs (the intermediate languages are instead put 133 under GPL). Of course, we could rediscuss 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 coexisted 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} 126 180 127 181 \end{enumerate}
Note: See TracChangeset
for help on using the changeset viewer.