Re: [isabelle] lexical matters
On Tue, 18 Jan 2011, mark at proof-technologies.com wrote:
An LCF-style prover is reasonably correct by construction,
independently of concrete syntax input and output. Errors in the
internalization/ externalization do not multiply as quickly as genuine
Yes, I agree that the LCF style largely solves problems of
trustworthiness, and that the sort of problems it solves are the most
serious. But given that this has been solved (a long time ago),
shouldn't we tackle the remaining problems?
Trustworthiness is just one of many problems, and we have been able to
increase it in Isabelle gradually over the years.
Apart from that efficiency, accessibility, usability etc. are of general
importance to make our arcane provers acceptable to more people out there.
I often find myself in the situation of a formalistic fundamentalist when
speaking to people outside our community.
E.g. when you start moving towards serious Prover IDEs, what I've been
involved for quite some time now, you will find many more issues than the
rather trivial parse/print problem of the low-level term language. Of
course, I always try to keep as much immediate reliability as possible.
But I also feel one should separate concerns here: if you need extreme
trustworthiness, then you should export full theory and proof content to
some tiny external checker. The latter does not even need concrete syntax
in the traditional sense.
HOL0 could be one such checker, if it would be able to absorb huge
theories and proofs (traces of inferences). Then one could implement some
"HOL0" button in Isabelle.
This archive was generated by a fusion of
Pipermail (Mailman edition) and