[FOM] 187:Grand Unification 2 - saving human lives

[Roger Bishop Jones]

On Wednesday 02 July 2003  3:39 pm, Harvey Friedman wrote:
> This is a continuation of posting #186, and puts the proof
> checking project into a wider perspective.

...

> What is needed is an appropriate mathematically friendly
> functional programming language, with clear mathematically
> friendly semantics, which does not sacrifice much in the way
> of efficiency. Complete modularity, no side effects, where
> semantics is inherited from the standard semantics of
> mathematics, etc. It should be noted that there are plenty of
> important contexts in which efficiency is not even remotely at
> issue but correctness and specification is - for example, in
> the area of the design and implementation of complex user
> interfaces.

...

I'm afraid that Harvey continues to "re-invent the wheel" with
this line of enquiry.

Most of his ideas seem quite sensible, but none of them seem
new, and very many people have been engaged in the development
of such ideas for decades (some perhaps for half a century,
and that might include Martin Davis in his spare time!).

The idea that new languages will make the difference is
plausible, and has been tried many many times, with many
different ideas about what kind of new language will do
the trick.
Some of these have even been philosopher-logicians, such
as Martin Lof, whose constructive type theories became
popular in Computer Science precisely because he and
others argued that they would facilitate the development
of verified programs.

Modern functional languages are aguably an offshoot of
theoretical developments intended to underpin program
verification, also inspired by well known logicians.
When Dana Scott went to Oxford and began to work with
Christopher Strachey they addressed the problem of
giving mathematically precise semantics to programming
languages so that programs could then be formally
verified.  Even with the best discoverable mathematical
methods for describing programming languages the
specifications of traditional languages proved
intractably complex.  One effect of this was to
convince many academics that languages should be
designed with an understanding of what makes for a
tractable semantics, and the languages which emerged
from these insights were the predecessors of modern
functional programming languages.

Some of these are excellent programming languages,
and are far more productive for many purposes than
more traditional languages.
However, they have had little impact on the problem
of producing formally verified programs.

I wholly approve of Harvey's new found interest
in this problem domain, but I doubt that he has yet
found a way in which his talents can make a difference.

Roger Jones