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

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). http://concurrency.ch/Content/publications/Blaeser_Component_Operating_System_PLOS_2007.pdf 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_Based_Tool_for_Semantics_of_Programming_Languages http://fsl.cs.illinois.edu/index.php/K-Maude:_A_Rewriting_Ba...