🚀 go-pugleaf

Dave Gillett:
   	When we define our domain of discourse to be functions, which
   accept inputs and produce (we hope!) results, we are able to
   express the necessary properties for verification of each function
   in terms of predicates linking properties of the inputs to
   properties of the results.  Composition of functions leads to
   combination and simplification of intermediate predicates, and
   ultimately to the set of pre- and post-conditions which
   demonstrates (or, as appropriate, fails to demonstrate) that our
   composition has the properties which we wish it to have.

This is nice, not only for "proof of correctness", but for things like
designing optimizers.  I believe everybody is familiar with the way a
specific case can often be implemented more efficiently than a general
case?

   	This exercise is entirely in terms of functions and
   predicates, which are mathematical objects, and any well-defined
   functional notation is sufficient to allow us to proceed to proof.

   	By contrast, the majority of the literature that I have seen
   on the verification of procedural programs starts, instead, from
   the notion that a program is a "text".  Resolution of syntactic and
   semantic issues, in order to arrive at suitable objects for
   reasoning, becomes a major task; indeed, there is rarely time or
   space left for the actual proof itself.

yacc at its finest :-)

The way I understand it, the term "functional language" was invented
by Backus to describe the deficiencies he saw in the languages he'd
helped develop (fortran, algol). Since people don't talk about this
much, I should point out that he also talked about Applicative State
Transition systems (with formal functional programming as the
subsystem used to generate a state).

Raul Rockwell