My third relevant computer "experience:" When I enrolled at the University of Maryland in 1982, I had to sign up for a "weed-out" course as my introduction to the computer science department. The course CMSC 110P (the "P" was for Pascal, added that year in favor of Fortran) introduced us to some wacky notion called A Calculus of Computer Programming. The esteemed Ben Schneiderman apparently had his hand in the "book" that backed the material, which in reality was a half-ream of paper rubberbanded together.
The course was all about how to create proofs of code, starting with individual operations and moving up to entire functions. It was a very tedious process. If I recall correctly, the course introduced its own proof language, one that bootstrapped itself. (I wish I still had the manuscript since I can't remember what it looks like). Everyone in the class hated it. It drove me nuts initially, but it did make a big impression on me in terms of how difficult it was to code demonstrably correct functions. I remember spending half the semester on proving a few simple functions.
Wikipedia has some interesting pages about lambda calculus and functional programming languages. I never tried Haskell or ML. The notion of using functional languages to help in programming defect-free code sounds intriguing but also very tedious. Today I still recognize that creating correct code is a significant challenge. While it's not the same thing, I view TDD as my way of demonstrating similar levels of control over what I produce.
February 2004 March 2004 May 2004 September 2004 October 2004 January 2005 February 2005 September 2005 October 2005 November 2005 December 2005 January 2006 February 2006 March 2006 June 2006 August 2006 January 2007 February 2007 March 2007 April 2007 September 2007 October 2007 November 2007 December 2007 January 2008