[no subject]

[Andrzej Trybulec <trybulec@math.uw.bialystok.pl>]

I forward a part of a message that John Harrison sent me.

---------- Forwarded message ----------
Date: Fri, 27 Jun 1997 21:55:04 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
To: Andrzej Trybulec <trybulec@math.uw.bialystok.pl>

...........
P.S. If you haven't already seen them, you might like to glance at a couple
of Cambridge technical reports that are markedly Mizar-inspired:

  http://www.cl.cam.ac.uk/users/jrh/papers/style.html

  http://www.cl.cam.ac.uk/users/drs1004/reports/declare.ps
--------------------------------------------

I failed to get the #.ps file of the first paper ("unexpected end
of file"), but #.dvi is OK.
I found John's paper very interesting. He compares a number of
different systems. Main stress is on advantages and disadvantages
of declarative (Hqthm, Mizar) and procedural (e.g. HOL) style.
The second paper (of Donald Syme) is more technical, he desribes
a specific system in declarative style, but he discuss also some
general problems.

Andrzej Trybulec