Peirce is one of the most underappreciated American geniuses. He actually invented the existential and universal quantifiers before Frege, although nobody dispu

Peirce is one of the most underappreciated American geniuses. He actually invented the existential and universal quantifiers before Frege, although nobody disputes that both did so independently. Peirce's works are available here: http://www.iupui.edu/~arisbe/ http://www.iupui.edu/~arisbe/ . I strongly recommend anyone with an interest in formal logic to peruse them. His existential graphs are particularly interesting: http://www.jfsowa.com/peirce/ms514.htm http://www.jfsowa.com/peirce/ms514.htm. I love systems where you start with a trivially true theorem and then through simple operations build an arbitrarily complex theorem while being assured that, for whatever faults it may have, it is correct. That's how I view formal programming too. I start with the empty specification and the empty program and the latter trivially satisfies the former. Then I make a small change to the specification and make the according change to the program. As a matter of practice, my specifications take the form of unit tests plus comments. So it looks an awful lot like TDD, just with a greater awareness that not everything than can be specified can be tested. Refactoring is just any transformation of the program text that maintains the specification holds predicate.