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
