recently, as you might have noted by a previous post of mine, that American Mathematical Society published a series of articles on formal proofs in 2008 November. See: http://www.ams.org/notices/200811/ The articles are:
• Formal Proof by Thomas Hales • Formal Proof — The Four-Color Theorem by Georges Gonthier • Formal Proof — Theory and Practice by John Harrison • Formal Proof — Getting Started by Freek Wiedijk I read 3 of them in December (only scanned the four-color theorem one). It was quite a fantastically enjoyable reading. ( For some personal notes, see: Current State Of Theorem Proving Systems at the bottom of • The Codification of Mathematics http://xahlee.org/cmaci/notation/math_codify.html ) As you may know, codification of math has been a long personal interest. In fact, my logical analytic habit has made me unable to read most math texts, which are full of logical errors and relies on a “human” interpretation for its soundness and clarity. having read those intro articles from the AMS publication on current state of the art, i decided that i'm going to learn HOL Light. (tried to learn Coq before and the tutorial is problematic) One of the interesting finding was that almost all theorem proving systems are written in ML family lang, e.g. Caml, Ocaml. Of course, i heard of Ocaml since about 1998 when i was doing Scheme. Somehow it never impressed me from reading the functional programing FAQ. I have always been attracted more to Haskell, perhaps only because it is _pure_ in the sense of not allowing assignment. With that, ocaml has been “just another functional lang” in my mind. But now, seeing that most theorem proving systems used in the real world are in Caml, thus i made start to learn Ocaml now. (in fact, its root is a theorem prover) i wanted to add proofs as enhancement to my A Visual Dictionary Of Special Plane Curves. Also, had ambition to write more... about algebraic geometry and differential geometry and geometry with complex numbers. Proofs will be major part of these type of works. I can no longer tolerate traditional mouthy written-english proofs. They must be codified proofs. In this: HOL Light Tutorial (for version 2.20) by John Harrison September 9, 2006, there's this paragraph: “This fits naturally with the view, expressed for example by Dijkstra (1976), that a programming language should be thought of first and foremost as an algorithm-oriented system of mathematical notation, and only secondarily as something to be run on a machine.” Wee! That has been my view since about 1997. The only lang that adhere to that view i know of is Mathematica. (lisping morons don't understand a iota of it. See: • Is Lisp's Objects Concept Necessary? http://xahlee.org/emacs/lisps_objects.html • The Concepts and Confusions of Prefix, Infix, Postfix and Fully Nested Notations http://xahlee.org/UnixResource_dir/writ/notations.html ) btw, anyone know the source of that Dijkstra quote? Xah ∑ http://xahlee.org/ ☄ -- http://mail.python.org/mailman/listinfo/python-list
