Formal Methods Considered Obscure

[Note: In the following sections, by "Nobody", I mean lessthan 1% of proffessional programmers.]

Why programmers don't use formal methods

1. Nobody has ever seen a formal proof of a program, much less
   one that they still understood an hour later.
   


2. Nobody writes specifications in the same languages in which
   they write code.
   


3. Even important proponents of Formal Methods think it is
   "too difficult" to do detailed formal proofs of large
   projects.
   


4. You have to understand complex state spaces, and use complicated
   notation to use Formal Methods.
   


5. Programmers are not adequately trained to use Formal Methods.
   


6. Tools to assist developers do not exist, or are not readily
   available.
   


7. Nobody knows how much time it would save them.
   


8. They believe the Church-Turing thesis means you cannot write
   a total-correctness-proof checker.
   

How do we fix it?

1. Publish proofs in well-known programming languages
   


2. Develop specification notations in well-known programming
   languages
   


3. Build some large projects that are formally specified
   and verified.
   


4. Publish good descriptions of how proofs and programs are actually
   derived.
   


5. Most programmers passed Geometry and Triginometry in High
   School. This demonstrates the sort of facility in equational
   logic needed for correctness proofs. However, providing
   some curriculum in using these techniques is needed as well,
   since most current texts in the field (_Scientific Programming_
   etc.) use obscure, custom-built programming languages.
   


6. Provide open source tools for checking proofs, validating
   specifications, etc.
   


7. Educate people on the time-sucking-abyss of the run-break-fix cycle.
   Do studies of developing similar applications between groups
   who use formal methods approaches and those who do not.
   


8. Explain that the Church-Turing thesis does not
   prevent you writing a total-correctness-proof checker.
   

   As you may recall, Church-Turing construction of a contradiction works
   when the program/turing-machine in question attempts to partition
   the set of programs into

   1. programs which terminate on all inputs
      
   2. programs which do not terminate on all inputs
      
   
   and then modify that partitioning-program to make a contradiction.
   

   If instead our program/turing-machine partitions programs into:
   

   1. programs which we know terminate on all inputs
      
   2. programs which we do not know whether they terminate or not.
      
   
   the contradiction does not arise, even when the partitioner falls (as we would hope it would) into the first set. If you modify it by adding an infinite loop at the termination point, it will no longer adhere to the proof checking rules, and you have then moved it into the set of things whose termination status is unknown; however saying we don't know if something terminates does not lead to a contradiction.
   

Synergy

It turns out that several items, above, are interrelated. If we provide a formally specified and verified library of software which is used to build tools for specifying and building a
proof checking and specification validation suite, using literate programming techniques to make our specification, implemntation, and verification clear, we accomplish most of these fixes.

If we build up class notes for a training program to teach the notation and practices to programmers, we achieve more of them.

If we then study people's programming proficiency and reliability when they do and don't use these techniques, we achive all of them.