The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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