Re: [isabelle] Large bodies of knowledge



Hi Rene,

the L4.verified kernel verification would satisfy (1), I guess.

As for (2), the major pull and funding argument there was from the application domain to achieve a “big result” as you call it. It did lead us to make advancements in a number of technical areas interesting for interactive proof and software verification, i.e. new techniques/methods, increased automation, increased usability (e.g. the find theorems command in Isabelle came out of this project). Most importantly it was a stress test on tools and methods to deal with scale, which also lead to research for others, not just our project (e.g. it was a good argument for the increased automation provided by sledgehammer).

I think we listed most of these in the proposal, and they were motivators for us, but they were not the strong arguments that got the project through. Those were all based on impact of the project result.

Both sides of the argument did hold up in this case. Everything you listed below (tools, libraries, teaching/industry, dealing with scale) came to pass in some form or other, in addition to the overall result. The only thing we didn’t do much with was proofs by reflection, but that was just because it wasn’t needed in our application domain.

Cheers,
Gerwin

On 03.02.2014, at 3:35 pm, Rene Vestergaard <vestergaard.rene at gmail.com> 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
>
>
> ---
>
> Cross-posted to coq-club at inria.fr and hol-info at lists.sourceforge.net.
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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