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 logical errors.

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.


	Makarius





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