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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and