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

[Harvey Friedman]

Reply to Jones 12:11PM 7/8/03.

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

Since the "wheel" doesn't work very well, it needs to be reinvented.

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

I hope that they will have a major effect in combination with a 
number of other ideas that will be eventually presented.

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

There are some very natural and powerful ideas that apparently have 
not been absorbed by the community working on this. There are a 
number of reasons for this, including the fact that once large 
investments are made in such projects, it becomes difficult to start 
over from scratch. That creates difficulties with funding agencies 
and other practical problems. This is not intended as any kind of 
negative statement. E.g., Windows needs to be redone from scratch, 
but Bill Gates is dead set against that.

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

I would not have gone about this in this way. I don't know what his 
thinking is like now.

>
>Modern functional languages are aguably an offshoot of
>theoretical developments intended to underpin program
>verification, also inspired by well known logicians.

The work I saw in functional languages was missing many key ideas, 
including those needed to make implementation efficient.

It is always nice to see someone appreciate the work of "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.

This project is not the way I would like to go. There has to be a 
fundamental superfriendly redesign of programming languages to 
support any kind of suitably friendly verification of software. 
Certain focused situations in hardware, where chips are duplicated in 
the millions, is quite a different story.

The superfriendly redesigned programming languages I have in mind do 
not have any subtle semantic issues of the kind that the languages 
Scott et al were concerned with have.

>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

New? I have been thinking about these matters for over 30 years. If I 
didn't THINK I had some major ideas about this, I wouldn't be writing 
about it on the FOM. Actually that's not quite true: I would write 
about it with the MERE expectation that it would initiate a 
discussion that could lead to major ideas.

Everything I have seen in this area, so far, convinces me that 
although there are a number of good ideas, the approaches are 
fundamentally flawed from the outset, and these flaws propagate 
upwards into unacceptable user unfriendliness.

The PARADIGM SHIFT I discussed involving wholesale systematic 
development of decision procedures for FINITE fragments throughout 
mathematics is a completely OBVIOUS idea that, if widely understood, 
could/should radically change the research directions and 
perspectives of quite a number of logicians and logician types. One 
can certainly claim that this paradigm shift idea is NOT NEW, as you 
seem to be saying.

I have already practiced a little bit of what I preach: a paper of 
mine is appearing in Fund. Math. with a very detailed proof that 
decides all 3 quantifier sentences in set theory with epsilon,=, and 
there are only FINITELY many such up to tautological equivalence. 
Another paper of mine gives an example of a 5 quantifier sentence in 
epsilon,= that cannot be decided in ZFC without the addition of large 
cardinal axioms.

This is not focused enough to be particularly useful for automated 
proof checking. However, it is a rather RADICAL departure from the 
thinking of set theorists.

Also look at the letter from Schwartz in my posting of 4:08PM 7/3/03.

PS: As I have said earlier on the FOM, I am pressed for time, and 
probably won't get back to this until the Fall.

Harvey Friedman