# OCaml, Language syntax, and Proof Systems

#### Do you have a question? Post it now! No Registration Necessary.  Now with pictures!

•  Subject
• Author
• Posted on
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:

80=A2 Formal Proof by Thomas Hales
80=A2 Formal Proof80=94 The Four-Color Theorem by Georges Gonthie=
r
80=A2 Formal Proof80=94 Theory and Practice by John Harrison
80=A2 Formal Proof80=94 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
=E2=80=A2 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
=E2=80=9Chuman=E2=80=9D 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
been80=9Cjust another functional lang=E2=80=9D in my mind. But now, se=
eing 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
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:

=E2=80=9CThis fits naturally with the view, expressed for example by Dijkst=
ra
(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.=E2=80=9D

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:

=E2=80=A2 Is Lisp's Objects Concept Necessary?
http://xahlee.org/emacs/lisps_objects.html

=E2=80=A2 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
=E2=88=91 http://xahlee.org /

=E2=98=84

## Re: OCaml, Language syntax, and Proof Systems

Xah Lee wrote:

You may also appreciate the freely-available first chapter of my book OCaml
for Scientists:

http://www.ffconsultancy.com/products/ocaml_for_scientists/chapter1.html

And the freely-available first chapter of The OCaml Journal:

http://www.ffconsultancy.com/products/ocaml_journal/free/introduction.html

I also recommend Jason Hickey's book which, I believe, is due to be