Re: [isabelle] [Coq-Club] Large bodies of knowledge

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.


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.


On Feb 2, 2014, at 11:09 PM, Rene Vestergaard <vester at> 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.