1. 12

In this paper McBride uses dependent types to define a set of data types whose elements are known (at compile time) to be in order. Generic programs for insertion and flattening are put together to build algorithms like quicksort and deletion from balanced 2-3 trees in a correct-by-construction way (without having to work with proofs).

It is exhilarating being drawn to one’s code by the strong currents of a good design. But that happens only in the last iteration: we are just as efficiently dashed against the rocks by a bad design, and the best tool to support recovery remains, literally, the drawing board.

  1.  

  2. 4

    Well, I got to section 7 before getting completely lost. Fascinating stuff but sadly over my head.