Oberon and Maude I think make a good case for (parameterised) modules, both from being able to reason mathematically and their use at low level OS system.
I've been very slowly trying to combine the work in Maru with Composita to yield a modular and deterministic lisp (Composita uses managed memory without GC).
Naturally you'd want to layer something like Shen or Maude on top of this, to provide the equational proof-checking. The K language is a good example - it provides facilities to model new languages and semantics like racket.
I've been very slowly trying to combine the work in Maru with Composita to yield a modular and deterministic lisp (Composita uses managed memory without GC).
http://concurrency.ch/Content/publications/Blaeser_Component...
Naturally you'd want to layer something like Shen or Maude on top of this, to provide the equational proof-checking. The K language is a good example - it provides facilities to model new languages and semantics like racket.
http://fsl.cs.illinois.edu/index.php/K-Maude:_A_Rewriting_Ba...