Lambda the Ultimate

Assuming that one cause of software problems is insufficient coverage of the state space (so data goes into some range that causes the program to run in an unexpected and bad way), I wonder if one could approach that issue by trying to deal with the state space more explicitly: start with a null program and iteratively break it down and define its behaviour over the full state space, all the while proving that it is correct, eventually reaching a "full" program. (Perhaps only for restricted problem domains.)

What are the current best languages/tools/practices along those lines? In my head I have some image of a 'star trek'y interface, perhaps vaguely akin to the Subtext GUI, which allows the developer to 'see' how they are progressing in decomposing things. I realize visual approaches might well have issues as the decomposition gets ever more branching.

Thanks.

(I am actively reading up on things like Spin, MBSE, SPARKAda, etc. but have no practical experience with any such thing, so remain skeptical and clueless even after reading up on things.)

Verified Programming in Guru is a tutorial introduction to Guru:

GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs.

In comparison to Coq:

GURU is inspired largely by the COQ theorem prover, used for formalized mathematics and theoretical computer science, as well as program verification. Like COQ, GURU has syntax for both proofs and programs, and supports dependent types. GURU does not have as complex forms of polymorphism and dependent types as COQ does. But GURU supports some features that are difficult or impossible for COQ to support, which are useful for practical program verification. In COQ, the compiler must be able to confirm that all programs are uniformly terminating: they must terminate on all possible inputs. We know from basic recursion theory or theoretical computer science that this means there are some programs which really do terminate on all inputs that the compiler will not be able to confirm do so. Furthermore, some programs, like web servers or operating systems, are not intended to terminate. So that is a significant limitation. Other features GURU has that COQ lacks include support for functional modeling of non-functional constructs like destructive updates of data structures and arrays; and better support for proving properties of dependently typed functions.

The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen.

In Objects as Modules in Newspeak, Gilad Bracha et al. describe a way to avoid the coupling in inherent constructs found in many OO languages such as a global namespace, "static" stateful variables, globally accessible object constructors, etc.

We describe support for modularity in Newspeak, a new programming language descended from Smalltalk and Self. Like Self, all computation — even an object’s own access to its internal structure — is performed by invoking methods on objects. However, like Smalltalk, Newspeak is class-based. Classes can be nested arbitrarily, as in Beta. Since all names denote method invocations, all classes are virtual; in particular, superclasses are virtual, so all classes act as mixins. Unlike its predecessors, there is no static state in Newspeak, nor is there a global namespace. Top level classes act as module definitions, which are independent, immutable, self-contained parametric namespaces. They can be instantiated into modules which may be stateful and mutually recursive. Naturally, like its predecessors, Newspeak is reflective: a mirror library allows structured access to the program meta-level.

There's a lot in here that should be of interest to LtUers interested in object capability based security.

While re-reading some Alan Kay goodness, I was urged on to try to find information on Lucid, which led me to Gipsy. Unfortunately not a lot turned up. I did find a Masters thesis which talks about them plus Java (!?) which I now have to find time to actually read. Anybody know much about any of this?