Lockhart's Lament

Lockhart seems to agree with Dijkstra, that problem solving can be taught. But my mind fixed on something else in the paper. The much criticised geometry proofs mentioned on page 21 looks very much like programming. Why not use Haskell notation? Or even better, Coq? The proofs could be type checked and evaluated automatically. The students would learn to program at the same time they were learning geometry. They are learning to program now as well, they just don't know it, and would probably have difficulties to apply their newly gained knowledge in programming, due to the special notation used.

The programming approach would also allow the students to create theorems of their own to be used in future proofs, building a library of geometry as they go.

Even though I agree with Lockhart that problem solving should be emphasized instead of mechanical application of rules, by not using a formal system, he relies too much on human intuition in the proofs created. The informal proof on page 21-22 is elegant, but relies on the intuitive understanding of rotation and that rectangles have diagonals of equal length alternatively that rectangles have corners with right angles (both can not be the definition of a rectangle).