Overview

PML is a variant of the ML language (like  Standard ML or  OCaml) which focuses both on being able to prove programs and be really usable. The current version starts to fulfill both goals even if several major features are still under development (like a compiler or input-output). PML should also be usable to develop certified mathematics.

Current status: the core language has now stabilized and one can start writing proofs. Many examples are available in the examples and lib folders.

PML is not yet usable as a production programming language. It is still a research platform. Nevertheless, we will be grateful if you try it and report about your experience and problems.

Installation

To install PML, you need

•  darcs,
•  OCaml (>= 3.11),
•  findlib (can also do without ... with a little makefile editing),
•  dypgen (a very nice parser generator for OCaml) and
•  bindlib (the darcs version only).
•  Boehm's GC (it is possible to compile PML without its compiler and drop this dependency, see below) For best performance, use libgc 7.1 or more recent with the following compilation option:

CFLAGS="-O2" ./configure --enable-threads=posix --enable-thread-local-alloc --disable-gc-debug

•  llvm+clang: the svn trunk version with few modifications (it is possible to compile PML without its compiler and drop this dependency, see below)
  • follow  this installation instructions
  • apply this patch  http://lama.univ-savoie.fr/~raffalli/volatile.diff which extends OCaml bindings
  • apply this patch  http://lama.univ-savoie.fr/~raffalli/ocamlmake.diff which fixes two problems with installation of OCaml bindings
  • optionnaly, apply this patch  http://lama.univ-savoie.fr/~raffalli/inline.diff which allows some inlining of recursive functions which llvm normally does not.
• If you do not want PML compiler, you don't need llvm nor Boehm's GC and you can set USELLVM=no and comment LLVMOCAMLLIBS in Makefile.config

Then, get the latest development version of PML, using darcs:

darcs get  http://lama.univ-savoie.fr/~raffalli/repos/pml

A  tar archive is also available (version 26/04/2013)

The above repository is a copy of PML which is manually updated from the working repository when this seems a good idea ;-). If you want to participate to PML's development, you may have a read write access to the working repository. Send an email to raffalli at univ-savoie.fr.

Then, follow the instructions in INSTALLDOC file at the root of the pml repository you just downloaded.

Using PML

•  Programming in PML (in progress): explains how to program in PML. These pages should converge toward a programming course based on PML, adapted even for beginners.

•  Proving in PML (planned): explains how to write properties and proof in PML. These pages should converge toward a course on certified programming (and may be later, certified mathematics).

• Programming and computer sciences courses in PML (in progress).

More details (page are signaled as "in progress" = readable or "planned" = not ready for reading)

• PMLExamples (in progress): examples that should help you to understand what PML is.
• PML99problems (in progress): some of the classical 99 problems in PML (source:  http://www.haskell.org/haskellwiki/H-99:_Ninety-Nine_Haskell_Problems)
•  manual (planned): not yet available, you can use a  draft pdf version : this should contain the formal description of the language.
•  Design goals (in progress): explains the idea behind PML. You need to know a few concepts about functional programming to understand this page.
• Design discussion (planned): current discussion about the design of PML.