[FOM] Formal verification

[Freek Wiedijk]

Hi Hendrik,

>Automath was written in Algol 60.  I hear that the system,
>and the translation of Grundlagen, have since been updated
>to work on modern systems.

Yes.  But Automath is awfully primitive by modern standards.
Also, it's spiritually very close to the Twelf system, which
still has an active user base, and has many more features.
So if you want to work in the Automath style, I'd take a
look at Twelf.

What's nice about Automath, is that its type theory is much
more regular than the modern type theories, at least IMHO
(my boss Herman Geuvers disagrees, I think :-))  Hardly
anyone knows about this though, the Automath type theory
has really been forgotten by the type theory community.

So to use Coq syntax, in Automath the two terms

	A -> B
	fun x : A => B

are the same thing

	[x : A] B

For a modern type theorist that's crazy, but the rules of
the type theory are really much nicer that way.  And it
still is perfectly useful as a logical framework.

Freek