Changeset 806


Ignore:
Timestamp:
May 13, 2011, 6:29:54 PM (9 years ago)
Author:
mulligan
Message:

more changes to language used

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/addenda/letter.tex

    r805 r806  
    120120
    121121\item The reviewers suggest we use this estimation to compare two possible
    122  scenarios: a) proceed as planned, porting all CompCert proofs to Matita or
     122 scenarios: a) proceed as planned, porting all the CompCert proofs to Matita or
    123123 b) port D3.1 and D4.1 to Coq and re-use the CompCert proofs.
    124124
    125125 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
     126 we now make a few points that we feel are important to understand our
    127127 perspective.
    128128 \begin{enumerate}
     
    134134   requirement, but for reasons I am not listing here we do champion open
    135135   source, in particular for software developed using public money.
    136   \item CompCert is surely part of the state of the art in compiler
     136  \item CompCert is without doubt part of the state of the art in compiler
    137137   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.
     138   trying to maximise simplicity and and potential for reuse. Nevertheless, some important design
     139   decisions have been taken from the very start of the CompCert effort that have not been
     140   questioned extensively. Among them, the use of a non-executable semantics
     141   for intermediate languages and the use of non-dependent types for the code.
    142142   From our point of view, the CerCo project is first of all a project in
    143143   compiler certification. Therefore, we are interested in exploring the
    144    design space for compiler certification. For this reason, already in the
     144   design space for compiler certification. For this reason, as early as in the
    145145   project proposal, we decided to start from different assumptions. In
    146    particular, we will favour dependent types and executable semantics.
     146   particular, we favour dependent types and an executable semantics.
    147147   We are not claiming in advance that we will obtain better results than
    148148   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
     149   solutions based on different techniques. We also note that the ones used
    150150   in CompCert are very reasonable because of the choice of Coq that,
    151    traditionally, has favoured the use of non executable, inductive
     151   traditionally, has favoured the use of non-executable, inductive
    152152   specification over executable ones.
    153153  \item If we decide to depart from the choices we made in the project
     
    160160   done in Matita to Coq. Since we have already used some features of Matita
    161161   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.
     162   obvious \emph{a priori} what solution would be more convenient.
    163163  \item It is clear that one partner is interested in promoting the use of
    164164   Matita. We think that more competition in the domain of interactive theorem
     
    168168   developed for Matita have already been ported to Coq itself, and the two
    169169   systems show alternative solutions for similar problems that are still
    170    under comparison (e.g. Matita's unification hints vs Coq type classes).
     170   under comparison (e.g. Matita's unification hints vs. Coq's type classes).
    171171   One of the major struggles of EU funded research, and FET in particular,
    172172   is the balance between innovation and stability. While the promotion and
    173173   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.
     174   it will provide some good outcomes `on the side', as it happened in the past when
     175   Matita was used for some major formalisations and new techniques were
     176   developed to solve recurring problems. This would be hardly possible using Coq, since
     177   nobody in the CerCo team is a member of the Coq development team and has the
     178   expertise to quickly modify such a large and complex system as Coq.
    179179 \end{enumerate}
    180180
Note: See TracChangeset for help on using the changeset viewer.