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 <[email protected]> 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 > ------------------------------------------------------------------------------ Managing the Performance of Cloud-Based Applications Take advantage of what the Cloud has to offer - Avoid Common Pitfalls. Read the Whitepaper. http://pubads.g.doubleclick.net/gampad/clk?id=121051231&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
