A nitpick. At top level: > Haskell/OCaml/Ada/F#/Coq (ML family of languages?) Then: > Languages like Ada might be better for experimental type stuff? It see

A nitpick. At top level: > Haskell/OCaml/Ada/F#/Coq (ML family of languages?) Then: > Languages like Ada might be better for experimental type stuff? It seems to me there's a confusion between Ada [1] and Agda [2], where Agda is what you meant. Ada is also interesting, but in the Pascal/Modula family and although strictly typed the type system is nowhere near as sophisticated as the ML family languages (and here too a big difference between real ML and dependently typed languages like Coq/Galina and Agda). Among the things I liked in Ada: - generic packages, a more disciplined way to have static genericity than C++ templates. One can declaratively constrain the input types to a generic package, with clean error codes. C++ concepts will close the gap and maybe be even more powerful, but Ada had this from day 1; - protected types for mutual access. A higher level mutual exclusion scheme than mutex. Add in Ada 95 IIRC; - integer subtypes, with ranges and automatic checks. Still I believe the train has passed, and nowadays rust (with some strong inspiration from the ML family) has more of a chance to make it as the next gen system programming language, although it'll take time. [1] http://www.adaic.org/ http://www.adaic.org/ [2] http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php