## OCaml, Language syntax, and Proof Systems

### OCaml, Language syntax, and Proof Systems

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.yqcomputer.com/
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://www.yqcomputer.com/
)

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
umaninterpretation 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 ust another functional langin 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:

his 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://www.yqcomputer.com/

The Concepts and Confusions of Prefix, Infix, Postfix and Fully
Nested Notations
http://www.yqcomputer.com/
)

btw, anyone know the source of that Dijkstra quote?

Xah
http://www.yqcomputer.com/

### OCaml, Language syntax, and Proof Systems

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

intro to ocaml, from official site
http://www.yqcomputer.com/

bjective CAML Tutorial most cited tutorial on the web
http://www.yqcomputer.com/

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
ntroduction to Caml http://www.yqcomputer.com/ ~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 mother *** ing abstruse jargons thru-
out, littering gospels about properties of starry-eyed *** ing
advantage of static mother *** ing 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 ARBAGE
COLLECTION tateful how something is xpression-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 mothe *** ing
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://www.yqcomputer.com/

Xah
http://www.yqcomputer.com/

### OCaml, Language syntax, and Proof Systems

> bjective CAML Tutorial most cited tutorial on the web >> http://www.yqcomputer.com/ >> >> The best one, is the one is >> ntroduction to Camlgt; > http://www.yqcomputer.com/ ~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.

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

http://www.yqcomputer.com/

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

http://www.yqcomputer.com/

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

http://www.yqcomputer.com/

--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.yqcomputer.com/

### OCaml, Language syntax, and Proof Systems

ust 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
aml.inria.fror the popularly cited tutorial at
caml-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 e don't allow
assignments and we have azy evaluationâ‚¬ I believed it for 10
years. No more.

Jon wrot>:
> And the freely-available first chapter of The OCaml Journa>: >>
> http://www.ffconsultancy.com/products/ocaml_journal/free/introduction.>. >>
> I also recommend Jason Hickey's book which, I believe, is due to >e
> 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/

On Jan 23, 4:36 pm, Jon H<rrop wr>te:
> Xah Lee wr>t>:
> > ok, i've been reading these Ocaml tutorials in the past few d>ys> >>
> > intro to ocaml, from official >i>e
> > http://caml.inria.fr/pub/docs/manual-ocaml/manual003.>tm> >>
> > bjective CAML Tutorial most cited tutorial on th> >eb
> > http://www.ocaml-tutorial>or>/> >
> > The best one, is the o>e>is
> > ntroduction to C>m> > > http://www.cs.jhu.edu/~scott/pl/lectures/caml-intr>.>tml
> > by Dr Scott Smith of Johns Hopkins U, apparently a lecture>n>te.
> > I found it by as one of the top result from google s>ar>h.
>
> You may also appreciate the freely-available first chapter of my book>OCaml
> for Scien>is>s:
>
> http://www.ffconsultancy.com/products/ocaml_for_scientists/chapter>.h>ml
>
> And the freely-available first chapter of The OCaml Jo>rn>l:

### OCaml, Language syntax, and Proof Systems

anguage, 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 WANT TO BELIEVEin

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 o 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 ost-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 omputer science R us

### OCaml, Language syntax, and Proof Systems

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://www.yqcomputer.com/

http://www.yqcomputer.com/

Xah
http://www.yqcomputer.com/