OCaml, Language syntax, and Proof Systems

[Xah Lee]

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/

☄