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/
☄
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 fuck, no concrete examples but full of high-horse abstract
terminologies that are factually from asses who doesn't know a flying
fuck about symbolic logic, replete with computer engineering fuck
typical of compiler geekers like garbage collection, garbage
collection, garbage collection!!!, memory address memory address
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
stupid unreadable fuck. The Haskll community is almost stupid. What
they talk all day is about monads, currying, linder myer fuck type.
That's what they talk about all day. All day and night. Monad! What's
a monad! The importance of monad! How to learn monad! Simple intro to
monad! Fucking morons, but MONAD!
PS i started a Ocaml learning blog here:
http://xah-ocaml.blogspot.com/
Xah
∑ http://xahlee.org/
☄
From: Dimiter "malkia" Stanev
Subject: Re: OCaml, Language syntax, and Proof Systems
Date:
Message-ID: <gldkml$n8q$1@news.motzarella.org>
> The haskell tutorials you can find online are the most mothefucking
> stupid unreadable fuck. The Haskll community is almost stupid. What
> they talk all day is about monads, currying, linder myer fuck type.
> That's what they talk about all day. All day and night. Monad! What's
> a monad! The importance of monad! How to learn monad! Simple intro to
> monad! Fucking morons, but MONAD!
I've tried to grok MONAD, and so far it goes like this:
Basically in shell terms:
# ls -lR . | find me$
ls would list all files recursively and would give that as an argument
to find. Not only that, but if the environment has changed "find" would
see that. In the case of BASH/SH/etc. and unix tools that environment is
the environment (PATH=blah:duh:, PROMPT=ddduh).
So to me monads, are simply forcing certain operations to go in sequence
where the result of the previous goes to the next, and the whole
environment is kind of copied with the changes that needed to.
This way you still don't have side effects, you somehow keep the old
world (environment), and produce a new one, and give it to the next
process + the result from the previous operation.
The difference with the shell programming, is that "ls" might do
something destructively to the environment (kill files, who knows),
while with monads, "find" would receive a copy of the world from before
"ls" was started + the changes it made and the result from the operation
and all that would be given to "find".
Off course - I still do not understand monands, but I'm trying... :)
Xah Lee wrote:
> 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/
>
> 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.
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
published by Cambridge University Press soon:
http://www.cs.caltech.edu/courses/cs134/cs134b/book.pdf
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
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
practices or paradigms.
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
about 4 online tutorials or downloadable paper-published books. They
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
spent on huge garbage texts about reading why haskell is better or
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
haskell by my enthusiasm. See: A Haskell A Day http://xahlee.org/haskell/haskell.html
(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.
Jon wrote:
> 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
> published by Cambridge University Press soon:
>
> 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 Harrop <····@ffconsultancy.com> wrote:
> Xah Lee wrote:
> > 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/
>
> > 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.
>
> 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...
>
> I also recommend Jason Hickey's book which, I believe, is due to be
> published by Cambridge University Press soon:
>
> http://www.cs.caltech.edu/courses/cs134/cs134b/book.pdf
>
> --
> Dr Jon D Harrop, Flying Frog Consultancy Ltd.http://www.ffconsultancy.com/?u
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
haskell.
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/
☄
Addendum:
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/
☄