The Coq mailing list

[Rene Vestergaard <vestergaard.rene AT gmail.com>]

Dear Vladimir,

Thank you for sharing your considerations.

I must have misrepresented my position in the rush to ask my questions.

My intention was to cover what you state as being important under 
'retrodiction', and it *is* the primary scientific justification I will 
be putting forward for the project. More, the monograph in question fits 
your description of the type of article you would want addressed, I believe.

My questions were about existing big formalizations, not so much what I 
had done.

Cheers,
Rene

On 2/3/14, 11:18 PM, Vladimir Voevodsky wrote:
> Let me express my opinion which is somewhat against what you say.
>
> I would be very interested in seeing the results of a project aimed at 
> rigorous formalization of all levels of reasoning in a relatively small 
> scientific paper which involves experiment(s). May be one of the classic 
> papers in biology.
>
> I think achieving such a goal is highly non-trivial, visionary and  important 
> undertaking.
>
> I would be much less interested in seeing the results of a project which would 
> formalize a large monograph in the ``industrial" style i.e. without paying 
> attention to the new ideas which arise in the process and aiming only at obtaining 
> the final result.
>
> Vladimir.
>
>
>
>
> On Feb 2, 2014, at 11:09 PM, Rene Vestergaard 
> <vester AT jaist.ac.jp>
>  wrote:
>
> > I will shortly be attempting to reach a, for us, non-standard audience with a 
> > project that includes the verification of the complete reasoning in a 
> > molecular-biology monograph.
> >
> > The primary sales argument is by proxy: there’s a Curry-Howard component to 
> > the project that allows us to solve an open problem in the application domain.
> >
> > The primary scientific argument concerns formal reasoning, including the 
> > value of formalising/verifying a large body of knowledge, be it a textbook, a 
> > monograph, a “big” result, or similar.
> >
> > I have my own personal arguments for why large applications are a good idea:
> > - tests of and guidance for maturity/naturalness/expressivity of tools and 
> > methodologies,
> > - development of libraries/momentum/etc.,
> > - teaching/industrial/etc. purposes,
> > - retrodiction and, of course,
> > - assuring large case splits and proof by reflection.
> >
> > I was hoping people would help me with
> > 1) what big applications have been done? what arguments were used?
> > 2) do the arguments hold up in retrospect?
> >
> > While 1) can be answered by references, I am particularly hoping that some of 
> > the people behind these projects would attempt to answer 2) as best as 
> > possible.
> >
> > Cheers,
> > Rene