RE: Mizar Syntax

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

On Mon, 28 Dec 1998, Frode L. Odegard wrote:

> Perhaps the best thing to do would be to start with an abstract
> syntax?  Once that has been nailed down, it is easier to discuss
> alternatives in the concrete syntax.
> 

You are right, of course. Actually the message you had cited was related
to the work on abstract syntax. There are two different things:

1. The requirement that a scheme must be justified by a proof, that
   again may be split:
  1.1 An implementation restriction
  1.2 The abstract syntax
2. Concrete representation, e.g. what I wrote that eventually the word
  "proof" will be omitted.

However, we are quite concerned with the concrete syntax. Because of
two reasons:

1. For the user a comfortable syntax is more important that
   intricacies of semantics.
2. Semantics evolves faster than concrete syntax. (the same goes
   for natural languages).

Happy New Year,
Andrzej