Static types or static analysis? * KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs http://llvm.org/p

Static types or static analysis? * KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs http://llvm.org/pubs/2008-12-OSDI-KLEE.html * Erlang Dialyzer http://www.erlang.org/doc/man/dialyzer.html * Datalog based systems http://www.cse.msu.edu/~cse914/Overheads/mmcgill-java-static-race-detector.pdf If you want static analysis hard coded into your language - what feature set do you want to support? The following support different styles of programming thus have very different static type systems. * Standard ML / OCaml * Haskell * Scala * Typed Racket * Qi And there's still the question that some kinds of extremely useful programs are very difficult to write in popular languages with strong static typing. miniKanren, a flexible embedding of Prolog and Constraint Logic Programming into Lisp, comes to mind here. I've seen versions of miniKanren written in Haskell and it abandons the most powerful feature of miniKanren - it can be trivially applied back on the language it is written in!