| 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 | 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} |
