PML (Proved ML)

This is source code, the date is the date of the initial check-in in the version control systemPML is a variant of the ML language (like SML 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 basic data types like char or machine integers). 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, I will be grateful if you try it and report about your experience and problems