Re:Formal correctness proofs -- YES! (Score 1)

As for all the people who hate parens in LISP or Scheme, check out DrScheme, the free, open-source Scheme interpreter from Rice University (URL escapes me right now, but I know it's below cs.rice.edu).

http://www.cs.rice.edu/CS/PLT/pack ages/drscheme/

Looks pretty darn slick.