This kind of work should get much more attention than it does. It's non-trivial, fairly new and does something potentially very useful (which is more than I can say for most "X in JavaScripts" things submitted here).
I don't understand enough to know how significant this work is. They present a system to infer dependent types, which, if it works well, would solve at least part of the problem of dependent types as I understand it: having to write out tons of type annotations all over the place.
Having never used dependent types, perhaps I'm just being romantic, but it seems that even having some constraints on just a few types (numerics, arrays/lists, perhaps strings), would be a great boon, and I hope one day we'll have a "commercial" (that is, useful with great tooling) language that supports dependent types.
I'd be happy with an extension to an existing language, that added a little new syntax. So you give the extended source to the new tool, it verifies type safety, and then strips the new syntax elements and passes it off to the original language's compiler. This can't be that hard, can it?
Microsoft Research created Spec#, which extends C# to have Eiffel-style contracts (pre- and post-conditions) specified above a function body. While the requires and ensures aren't dependent types, they do allow for extended static checking via Microsoft's Z3 theorem prover.
This was a great talk! I was excited to see that there's (or was) some work being done to extend GHC to support this: http://goto.ucsd.edu/~rjhala/liquid/
Thanks! It's great to see interest in our work on HN. Yes, this is the precursor to and basis for our current work on refinement type inference for C.
For those who haven't seen it, our recent work has focused on extending the automatic program verification techniques shown in this talk to work for low-level programs - that is, programs that use mutable state, pointer arithmetic, and so on. The project page for our Liquid Types-based verifier for C programs is here: http://goto.ucsd.edu/csolve/
