Lambda the Ultimate

The Intuitionistic Programming Language purports to do nifty things:

The semantics of IPL is based on intuitionistic type theory extended with a component model it compiles to LLVM bytecode using a novel algorithm based on term rewriting. The IPL compiler is very small: less than 10,000 lines of OCaml code.

IPL provides

zero abstraction penalty,
a very high level of abstraction,
excellent run time performance,
strong static safety guarantees,
predictable performance without GC pauses,
support for verification and testing, and
a composable effect system based on free monads.

The combination of these features is made possible by an algorithm that eliminates high level constructs at compile time. The limitation implied by this algorithm is that mutable complex state has to be region based (global or local).

IPL is currently in the early stages of development and there are many opportunities to make a large impact on its future direction and for further innovation in the space.