Total functional programming (and the associated analysis of codata has already been touched on), so I'll just address your interest in static guarantees for sp

Total functional programming (and the associated analysis of codata has already been touched on), so I'll just address your interest in static guarantees for space usage. The Virgil programming language[1] has been designed with exactly this in mind. It is aimed at embedded systems where memory is extremely constrained and running out of memory could kill people. Heap allocation is not possible in the language and all data structures are initialized during compilation (like C++ templates, but more sophisticated). The compiler can use the initialization information for advanced optimization and analysis as well as serving as a bound on the memory usage. [2] The language also has some interesting static typing ideas, but they are not as distinct from other languages. Further discussion on LtU: http://lambda-the-ultimate.org/node/2131 http://lambda-the-ultimate.org/node/2131 [1] https://code.google.com/p/virgil/ https://code.google.com/p/virgil/ [2] http://compilers.cs.ucla.edu/virgil/overview.html http://compilers.cs.ucla.edu/virgil/overview.html