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