# OCaml, Language syntax, and Proof Systems

X

#### 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
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/

â˜„

X

#### Xah Lee

ok, i've been reading these Ocaml tutorials in the past few days:

intro to ocaml, from official site
http://caml.inria.fr/pub/docs/manual-ocaml/manual003.html

â€œObjective CAML Tutorialâ€, most cited tutorial on the web
http://www.ocaml-tutorial.org/

None of them are perfect, but much better than haskell ones.
The official tutorial is ok, but still confusing.

The one at ocaml-tutorial.org is somewhat but mostly because it's a
lot more explanatory text. It has much verbiage for imperative
programers (i.e. half of the text is about Perl this, C that, Java
thus, trying to each you functional lang by comparative study assuming
you are one of these these idiots. Half of the time, the comparison
doesn't make much sense)

The best one, is the one is
â€œIntroduction to Camlâ€
http://www.cs.jhu.edu/~scott/pl/lectures/caml-intro.html
by Dr Scott Smith of Johns Hopkins U, apparently a lecture note.
I found it by as one of the top result from google search.

This one is to the point, on lang syntax, what they do and mean, to
the point short examples, focusing one concept at a time. (as opposed
to the typical of: littering of motherfucking abstruse jargons thru-
out, littering gospels about properties of starry-eyed fucking
advantage of static mother fucking typing, the beauties of functional
programing ****, no concrete examples but full of high-horse abstract
terminologies that are factually from asses who doesn't know a flying
**** about symbolic logic, replete with computer engineering ****
typical of compiler geekers like garbage collection, garbage
memory address, pointers pointers pointers!!! hips and stacks and hips
and stacks and very hip!)

though, it is of course not my ideal, because it still now and then
mention extraneous stupid computer engineering concepts like â€œGARBAGE
COLLECTIONâ€, â€œstatefulâ€, how something is â€œexpression-basedâ€, etc. If
you are have a computer science background, sure these are no problem.
But if you are a say practical programer who never took computer
science classes, you'll go Huh? and if you are say the world's top
mathematician but never studied programing, you'll go HUH?

But again, this tutorial is far far better than vast majority of
tutorials out there about functional programing (except mine).

The haskell tutorials you can find online are the most mothefucking
they talk all day is about monads, currying, linder myer **** type.
That's what they talk about all day. All day and night. Monad! What's

PS i started a Ocaml learning blog here:
http://xah-ocaml.blogspot.com/

Xah
âˆ‘ http://xahlee.org/

â˜„

X

#### Xah Lee

Just a quick relpy.

Jon's tutorial:
http://www.ffconsultancy.com/products/ocaml_for_scientists/chapter1.html

is by far the best tutorial of Ocaml.

It is far better than the official intro to ocaml at
â€œcaml.inria.frâ€ or the popularly cited tutorial at
â€œocaml-tutorial.orgâ€ .

Jon's tutorial, namely the free chapter 1 of his book, is concise, to
the point, well written, well organized, does not unnecessarily use
abstruse jargons or concepts, does not pitch or preach engineering

Jon's book title says it all: Ocaml for Scientist.
Scientists are intelligent. All programing language tutorials should
be modeled like this. For some detail, see:

â€¢ Examples Of Quality Documentation In The Computing Industry
http://xahlee.org/perl-python/quality_docs.html

Btw, i've learned far more Ocaml in the past 3 days than the about 1
month of full time trying to learn Haskell. Mostly in 2006 or 2007. I
did not even obtain a basic understanding of the syntax. I do not have
a basic understanding of its types or how to define a type (was quite
confused in this). I don't even have a good idea what the lang's
syntactical elements or structural elements or semantic elements. In
fact, i have no basic understanding of the language. I tried. I tried
are extremely low quality and or idiotic. Half of the time is wasted
on finding a good tutorial or reading unreadable ones, and time is
currying this or monads that (they idiots lacking mathematician's
perspicacity don't really understand the subject). Motherfucking
idiots. (i even tried to start a mailing list and drew a web-badge for
(it went no where and is now on hold indefinitely))

I really believed in Haskell, almost just by its â€œwe don't allow
assignments and we have â€˜lazy evaluationâ€™â€. I believed it for 10
years. No more.
And the freely-available first chapter of The OCaml Journal:

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

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

http://www.cs.caltech.edu/courses/cs134/cs134b/book.pdf

Thanks. Am still reading your chapter 1 yet. Will check those out
later.

Xah
âˆ‘ http://xahlee.org/

â˜„

X

#### Xah Lee

Language, Purity, Cult, and Deception

Xah Lee, 2009-01-24

[this essay is roughly a 10 years personal retrospect of some
languages, in particular Scheme and Haskell.]

I learned far more Ocaml in the past 2 days than the fucking 2 months
i tried to learn Haskell, with 10 years of â€œI WANT TO BELIEVEâ€ in

The Haskell's problem is similar to Scheme lisp, being academic and of
little industrial involvement. About 10 years ago, during the dot com
era around 1999, where scripting war is going on (Perl, tcl,
Applescript, Userland Frontier, with in the corner Python, Ruby, Icon,
Scheme, in the air of Java, HTML 3, CSS, CGI, javascript), i was sold
a lie by Scheme lisp. Scheme, has a aura of elegance and minimalism
that's one hundred miles in radius. I have always been a advocate of
functional programing, with a heart for formal methods. Scheme, being
a academic lang, has such a association. At the time, Open Source and
Linux have just arrived on the scene and screaming the rounds in the
industry, along with Apache & Perl. The Larry Wall scumbag and Eric
Raymond motherfucker and Linus T moron and Richard Stallman often
appears in interviews in mainstream media. Richard Stallman's FSF with
its GNU, is quick to make sure he's not forgotten, by a campaign on
naming of Linux to GNU/Linux. FSF announced that Scheme is its chosen
scripting lang for GNU system. Plans and visions of Guile â€” the new
Scheme implementation, is that due to Scheme Lisp's power will have
lang conversion abilities on the fly so programers can code in other
lang if they wanted to, anywhere in the GNU platform. Around that
time, i also wholeheartedly subscribed to some A Brave Gnu World
bulletin of FSF with high expectations.

Now, it's 2009. Ten years have passed. Guile disappeared into
oblivion. Scheme is tail recursing in some unknown desert. PHP
practically and quietly surpassed the motherfucking foghorn'd Perl in
early 2000s to become the top 5 languages. Python has surfaced to
became a mainstream. Ruby is the hip kid on the block. Where is
Scheme? O, you can still hear these idiots debating tail recursions
among themselves in newsgroups. Tail recursion! Tail recursion! And
their standard the R6RS in 2007, by their own consensus, is one fucked
up shit.

In 2000, i was a fair expert in unix technologies. Sys admin to
several data center's solaris boxes each costing some 20 grands.
Master of Mathematica and Perl but don't know much about any other
lang or lang in general. Today, i am a expert of about 5 languages and
working knowledge with tens or so various ones. There is nothing in
Scheme i'd consider elegant, not remotely, even if we only consider
R4RS.

Scheme, like other langs with a cult, sold me lie that lasted 10
years. Similarly, Haskell fucked me with a tag of â€œno assignmentâ€
purity. You can try to learn the lang for years and all you'll learn
is that there's something called currying and monad. I regret i
learned python too in 2006. Perl is known for its intentional
egregious lies, lead by the demagogue Larry Wall (disclaimer: opinion
only). It fell apart unable to sustain its â€œpost-modernisticâ€
deceptions. Python always seemed reasonable to me, until you stepped
into it. You learned that the community is also culty, and is into
certain grand visions on beauty & elegance with its increasingly
complex syntax soup with backward incompatible python 3.0. The python
fuckheads sport the air of â€œcomputer science R usâ€, in reality they
are idiots about the same level of Perl mongers. (Schemers and Haskell
people at least know what they are talking about. They just don't have
the know how of the industry.)

I think my story can teach tech geekers something. In my experience,
the langs that are truely a joy to learn and use, are those sans a
cult. Mathematica, javascript, PHP, are all extremely a joy to use.
Anything you want to do or learn how to do, in so far that the lang is
suitable, can be done quickly. Their docs are to the point. And today
i have to include Ocaml. It's not about whether the lang is
functional, or whether the lang is elegant, or what theoretical power
it has. Also, lang of strong academic background such as Scheme and
Haskell are likely to stay forever there, regardless what is the
technical nature of the lang. The background of the community, makes
half what the language is.

Disclaimer: All mentions of real persons are opinion only.

Xah
âˆ‘ http://xahlee.org/

â˜„

X

#### Xah Lee

The above is not a terrible insight, but i suppose it should be useful
for some application. Today, there's huge number of languages, each
screaming ME! To name a few that are talked about by geekers, there's
Arc, Clojure, Scalar, F#, Erlang, Ruby, Groovy, Python 3, Perl6. (for
a big list, see: Proliferation of Computing Languages) So, if i want
to learn another lang down the road, and wish it to be a joy to use,
usable docs, large number of usable libraries, or well supported,
practical community that doesn't loop into monad or tail recursion
every minute, then which one should i buy? With criterions of
industrial background, not culty, lang beauty matter not that much, in
mind, i think Erlang, F# would be great choices, while langs like Qi,
Oz, Arc, Perl6, would be most questionable.

Perm url:

â€¢ Language, Purity, Cult, and Deception
http://xahlee.org/UnixResource_dir/writ/lang_purity_cult_deception.html

http://xahlee.blogspot.com/2009/01/language-purity-cult-and-deception.html

Xah
âˆ‘ http://xahlee.org/

â˜„

You'll need to choose a username for the site, which only take a couple of moments. After that, you can post your question and our members will help you out.

### Members online

No members online now.