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.