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

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

- 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)

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

I rather agree with Philippe Audebaud's observation after working on the **tmcoq**
TeXmacs interface for Coq:
[the] introduction of the

(see http://tmcoq.audebaud.org/)
`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.

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).

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

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

This topic: PG > NotesOnProofLanguages

Topic revision: r1 - 05 Sep 2006 - 21:13:38 - DavidAspinall

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies