Re: [isabelle] Proof by analogy and proof stability in Isabelle



On Fri, 30 Apr 2010, Dave Thayer wrote:

I think an important aspect of this topic is the issue of legal liability. If you use a theorem prover to prove a theorem, that is used to create a query into a medical ontology, which is then used in the diagnostic train for determining a patients treatment protocol you better be able to stand up in court and defend it. I would not want to tell a judge: "at this step we invoke the magic word 'auto' which does 'something unknown' and then we went on from there'.

While Isabelle is a very complex system, internally everything is reduced to basic principles, and run through an LCF-style inference kernel. The kernel can also produce explicit proof objects as a backup, although this degrades performance greatly. Even without proof terms, the type-safety of Standard ML gives certain static guarantees (in contrast to OCaml, or other much less rigid languages).

This does not mean that the system only produces ethernally true results -- there are other influences beyond a certain architecture and properties of the implementation languages.

Nonetheless, I would characterize our tradition of theorem proving as "fundamentalist" in the sense that everything is based on proper definitions and proofs.


	Makarius





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