Notes on the design of proof languages

(essay under construction: please do not comment/revise yet)

A proof language is a formal language for writing mathematical proofs, inside proof scripts.

Incremental interpretation

• The importance of feedback during development: incremental compilation/checking versus batch checking
• The nature of useful feedback
• Distinction between goal-oriented proof development (backwards proof style, explaining what remains to be solved) and formalising forwards proofs (explaining context)

Modular structure and proof reuse

Versioning

• Mizar's use of versions
• Development graphs applied in Inka/Omega

Dynamically extensible syntax

I rather agree with Philippe Audebaud's observation after working on the tmcoq TeXmacs interface for Coq: [the] introduction of the Notation mechanism in Coq version 8.0 has results, IOMO, in a serious regression with respect to what history of programming languages has learn to us. This mechanism allows dynamic change in the way source code is understood at the level of the lexer/parser, in the same spirit as TeX commands permits. More importantly, this makes confusion between structure and rendering. Good programming practice would rather suggest to put away Notation from Coq source. (see http://tmcoq.audebaud.org/)

The problem is that informal mathematical practice does afford this rich kind of freedom to the author. For example ...

A sensible way around this seems to be a careful distinction between the syntax used for mathematical formulae, which may be freely dynamically extended, and the syntax used for the proof language itself, which ought to be more controlled. In Isabelle/Isar, this is the distinction between the inner and outer syntax; the inner syntax is even warmly embraced in string quotation marks.

The current philosophy of the Proof General interface is to ignore the inner syntax for a system, and to try to get the system itself to explain the outer syntax for a system, in a standard way. Thus we recognise parts of the proof language which introduce the start of a proof and which end a proof, and parts which are steps in between. Other parts of the proof language introduce definitions or declarations. Our thesis is that we can get quite far with surface-level understanding of this structure, occasionally using the system itself to embelish with additional information (for example, dependencies between elements).

Genericity

Can we have a generic proof language? Isar was designed in principle to be generic, but its only implementation was inside Isabelle and by now its mechanisms are rather closely embedded.

• specifically
• design of modular module languages

-- DavidAspinall - Sep 2006

References

• Wenzel's thesis
• Freek Wiedijk's [http://http://www.cs.ru.nl/~freek/comparison/index.html][17 Provers of the World]]

Discussion