Dependent-type 'revolution'

Just prior to Scala eXchange 2012 (which took place earlier this week), I came across a (quite accessible) blog post entitled, Unifying Programming and Math - The Dependent Type Revolution.

An intriguing title, referring to one of those subjects I hadn't quite got round to investigating yet - still on my to-do list was to listen to an interview with Miles Sabin talking about, amongst other things, dependent types.

Although Miles was at the conference on the first day, he wasn't around on the second, so I missed my chance to talk to him. However, there was always the panel discussion, so I made do ;-) with addressing a question to Martin Odersky on the matter (22:20 mins into the video).

Here's what he had to say, with my own, possibly wrong-end-of-the-stick, embellishments:

• There's an interesting area between Haskell and maths, that's populated by programming languages [featuring dependent types] such as Agda, and theorem provers such as Coq.
• According to the Curry-Howard Isomorphism,
• there's a strong correspondence between types and properties [of programs] (so we can encode the properties of programs in types);
• [By properties of programs is meant things like the property of associativity of the concatenation operator of a list.]
• if a type is a property [of a program], then the [existence of that working] program [involving that type] is a proof of that property.
• Certain theorems in maths (e.g. Four-colour theorem) can only be proved (practically) by writing a program [in a language like Agda, expressing the theorem as dependent types].
• Applications of such proofs in computing are currently somewhat specialised/limited:
• proof of correctness wrt attacks on cryptographic systems.
• proof of correctness of whole programs, using theorem provers such as Z3 to do the constraints solving, is currently limited to programs in the 10s of lines.
• Scaling of proof of whole-program correctness to much larger programs, or the obviation of unit tests, is unlikely to happen any time soon.
• We are constrained by the need to reconcile that which it is possible to do with types, with that which humans can comprehend.
• Having type systems which are easy to use is the more pressing challenge.

To delve deeper into dependent types using Scala, it looks like Miles Sabin's Shapeless project and blog are the places to go.