Re: [Caml-list] Nicely written Caml/OCaml code to read.

["\"Mark Adams\"" <mark@proof-technologies.com>]

Hi Clement,

My HOL Zero program may be of interest to you.  It's a theorem prover (i.e.
a program for performing mathematical proof), but don't let that put you
off!  It's written in about 8,000-9,000 non-blank/non-comment lines of
OCaml, and is heavily commented, nicely formatted and implemented in a
straightforward style.  I've tried to make it as easy as possible for others
to understand the implementation (the idea is that people will then trust
that the proofs it performs are correct), and it comes with a glossary
explaining background terminology about theorem provers.  There is no use of
Object-Oriented, there is only a little optimisation (to do basic sensible
things regarding tail recursion, etc) and it has a simple implementation of
trees.

    http://www.proof-technologies.com/holzero.html

To run it, you'll need a Unix-like operating system with bash, OCaml and
Camlp5.

There is even a $100 bountry reward if you manage to find a fundamental flaw
in the mathematical soundness of the program!

Mark Adams
Proof Technologies Ltd


on 13/4/11 9:40 PM, Create Software <createsoftware@users.sourceforge.net>
wrote:

> Hi all,
>
> I'll be taking exams at the end of the year (starting in a week,
actually),
> which include programming / informatics
> tests. The language used in these exams is Caml Light (you guessed right:
> grandes écoles).
>
> I've done a lot of programming in previous years, but I didn't know
> Caml/OCaml before high school -- I come from a mixed
> C++/C# world, with drops of Python here and there.
>
> In developing my skill in other languages, I always found that reading
good
> code at some point was a great boost to the
> beauty and cleanness of the programs I wrote. Usually, every language has
> it's own conventions, best practices, and I
> think you can usually learn a lot by reading well-written, nicely-crafted
> code.
>
> So here's my question: **which code would you recommend to read?**
>
> (As a side note, I'm not really interested (at least in the very short
term)
> in anything on the object-oriented side of
> the language, since the notions used at the exam are limited to the
elements
> available in Caml Light.)
>
> I've tried batteries and Jane street core/ext-core libraries, but the
former
> has extremely few comments, and the latter
> is too widely optimized to be enjoyable to read (Jane street's map
function
> is 30 lines long due to loop unrolling).
>
> Anything that deals with trees or finite state automata gets extra brownie
> points =) (and +2 if Gabriel Scherer answers)
>
> Thanks for your help!
> Clément.
>
> --
> Create Software - Open source, lightweight, and efficient software -
> @createsoftware <http://twitter.com/createsoftware>
> http://createsoftware.users.sourceforge.net -
> http://synchronicity.sourceforge.net
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>
>
>