🚀 go-pugleaf

In article <417@uqcspe.cs.uq.oz.au> paul@cs.uq.oz.au writes:
> [Does anybody know of RP using FP in Industry?]

It has been some while since I worked in industry, but when I was
there I was responsible -- with Geoff Burn -- for a distributed
implementation of a functional programming language.

We chose to formally specify our extension to the G-machine. I claim
that without making this executable, it is impossible to validate the
design in any reasonable time period. For the record the specification
extended over 50 pages [1,3].

I have previously proved correct a small sequential implementation of
a functional language. The specification was two pages, the proof was
60 pages and took 12 -- 18 months (see reference [2]).

To give you some idea of what would be involved in a formal proof, I
jot down some of the points that would need to be considered.

    (1) Abstract Interpretation: when it was permissable to rearrange the
        evaluation of sub-expressions.
    (2) Garbage Collection: Is it correct? How does it mesh with the
        machine?
    (3) Evaluation order: The G-machine sometimes performs eager
        evaluation. e.g. (x:xs) is built directly. This makes it more
        difficult to prove properties about.

This leads to Lester's Hypothesis:
    "In most industrial applications, a fully formal approach is
     not cost effective."

And as a Corollary:
    "Executable specifications provide a reasonable compromise between
     formality and cost."

I look forward to the day when this is not the case.

David Lester.

(Did I really send this from the current home of VDM?)

[1] @inproceedings{BURN88b,
author = "G.L. Burn",
title = "A Shared Memory Parallel {G}-Machine Based on the Evaluation
Transformer Model of Computation",
booktitle = "Proceedings of the Workshop on the Implementation of Lazy
Functional Languages",
address = {Aspen\"{a}s, G\"{o}teborg, Sweden},
year = 1988,
month = "5--8 September"
} 

[2] @phdthesis{LESTER88a,
author = "Lester, D.R.",
title = "Combinator Graph Reduction: A Congruence and its
Applications",
school = "Oxford University",
type = "DPhil thesis",
year = 1988,
note = "{\it Also} published as Technical Monograph PRG-73",
}

[3] @inproceedings{LESTER89c,
author = "Lester, D.R. and Burn, G.L.",
title = "An Executable Specification of the {HDG}-{M}achine",
booktitle = "Workshop on Massive Parallelism: Hardware, Programming
and Applications",
address = "Amalfi, Italy",
month = "9--15 October",
year = 1989
}