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

[Harvey Friedman]

Reply to Anderson  9:36PM  7/2/03.

>Regarding Dr. Friedman's latest posting concerned with the development of
>a verifiable programming language, I'm not sure I understand how what's
>being proposed would differ in practice from existing research
>languages, such as ML, that allow formal proofs of correctness.  What
>further benefits might be realized if a language meeting the
>specifications set out were to be created?
>
>Regards,
>
>Stuart Anderson

In #187, I wrote:

DESIGN AN APPROPRIATE LANGUAGE FOR SOFTWARE DEVELOPMENT WHICH 
SUPPORTS FRIENDLY DEVELOPMENT OF EFFICIENT CODE THAT IS SPECIFIED AND 
VERIFIED AS PROGRAMS ARE BEING DEVELOPED.

If this was done properly, and explained properly, then you could 
tell something happened. Here would be some consequences:

1. The military would require that all critical software developed 
under its contracts be specified by the military and/or contractor in 
the associated specification language, the code written in the 
programming language, a proof that the code meets the specifications 
provided by the contractor, and the proof verified by the standard 
core proof checker. Contracts would be obtained and performance would 
be met. Critical military code would be bug free. My recollection is 
that there was a naive move in this direction by the military with a 
programming language called ADA. This move by the military was 
decades too early, but the time will come for this.

2. There would be a mad scramble in the private sector to develop 
tools that would give software companies and/or their clients the 
ability to perform as required by the massively lucrative military 
contracts.

3. This in turn would largely refocus the computer science curriculum 
towards developing student competence in these new tools. Those most 
able to master these new tools would command enormous starting 
salaries.

4. Software specifications in the unclassified sector could be put 
out on the Internet, accompanied with a price. Anyone first providing 
the software together with a verified proof that the software meets 
the specifications, would get paid immediately. Since the correctness 
of the software developed would NOT be at issue, it would be trivial 
to force payment in Court. Prices for urgently needed software 
meeting complex specifications might be worth tens or even hundreds 
of millions of dollars. Conceivably someone with far greater 
understanding of and competence in the use of such tools than anyone 
else, or almost anyone else, would be able to REGULARLY make tens or 
even hundreds of millions of dollars just sitting in front of a 
computer and thinking, without even having to talk to a human being, 
let alone sitting for a job interview.

Last time I checked, this hasn't happened.

In order for this to happen, things have to be done very very very 
very very very very very very very friendly.

We might as well start over.

Harvey Friedman