[isabelle] Large bodies of knowledge
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
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
- development of libraries/momentum/etc.,
- teaching/industrial/etc. purposes,
- retrodiction and, of course, - assuring large case splits and proof by
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.
Cross-posted to coq-club at inria.fr and hol-info at lists.sourceforge.net.
This archive was generated by a fusion of
Pipermail (Mailman edition) and