Last modified 8 years ago Last modified on 06/11/09 21:21:06

PML's Design goals

Context and positioning of the project

Ever since FORTRAN appeared fifty years ago, Programming languages have been evolving rapidly. These languages now include more and more sophisticated concepts like "objects", "type inference", "modules"... This richness makes it more and more complex to train programmers and makes it difficult for them to follow the innovations and changes in programming languages.

Another phenomenon is the emergence of formal methods used in conjunction with various programming languages. This generally introduces another layer to languages in order to write specifications, and sometimes yet another one for proofs. Learning a programming language together with the associated specification/proof languages can take an important effort.

Projects such as ACL2, the successor of nqthm, the Boyer-Moore theorem prover uses a rather simple language (namely LISP) both as a programming language and specification language, allowing to keep a unity in the system. Unfortunately, LISP is limited both as a programming language (no good treatment of sum type, no module system) and specification language (very limited quantification). Moreover, LISP has no compile-time type-check and these could be very useful to detect bugs and automatically assert properties.

The aim of this project is to build a very powerful language (with no loss of expressive power compared to state of the art languages) based on a very small number of simple features. We think this will be possible thanks to recent progress both in the semantics of programming languages and the apparition of new algorithms for type inference based on constraints-solving. In fact, we propose in [RAF08b] an innovative concept derived from the later to enable this: constraints-checking.

Moreover, our language will be used not only as a programming language and as a specification language (like in ACL2), but also as a proof language. This is natural for an ML-like language because, for instance, pattern-matching is a natural and powerful way to make a case analysis in a proof. This also means that our tool will follow easely a light philosophy.

PML is different from the other modern programming languages because its design focuses on a few powerful concepts. One problem this raises is that it is more difficult for a compiler to produce efficient code. In particular, since PML unifies several notions of products (modules, tuples and records), there is no simple way to choose the internal representation of a product, especially with implicit subtyping. Writing a good compiler for PML will require more complex optimisations schemes (probably driven by typing) than languages like OCaml or Haskell.

Here is a simple example, accepted by the current version of PML, demonstrating product type, sum type and subtyping. We define ternary trees as an extension of binary trees with an implicit subtyping relation (all function accepting binary_trees will accept ternary trees, by ignoring the middle_son):

type rec binary_tree (A) =
  [ Nil[] | Node[A with val left_son : binary_tree(A) val right_son : binary_tree(A)] ]
type rec ternary_tree(A) =
  binary_tree({ A with val middle_son : ternary_tree(A)})

PML requires a termination criterion because a proof by induction will just be a normal recursive program. Such a program has to be well-founded in order to correspond to a valid proof. A subset of Haskell (a pure functional programming language developed in Chalmers) can now use Aprove to establish termination of simple programs. However, we want the test to be fully integrated with the language, and be compatible with very modular programs. At the moment, these goals seem difficult to achieve with Aprove or other external termination checkers.

PML's approach to proofs is very innovative because it can be seen as an intermediate level between the fully automated approach of ACL2 or PVS and the approach based on a specific formalism for proofs like Coq, ALF, Isabelle, ... The former proof assistants accept to use any automated theorem prover, with one main drawback: the correction of such a system are postulated a priori. The later proof assistants define proofs in a precise framework such as natural deduction, calculus of construction, <em>etc.</em> and provide tactics to build complex proofs. The proof are usually tedious to write and impossible to read or write without a specific interface. Even with a declarative language like Mizar (or the Mizar mode for Isabelle or Coq), it is not very easy to build proofs, let alone concise proofs!

PML logic is in fact the equational theory of its programming language and we plan to use variants of Knuth-Bendix completion as a proof-checker. The first experiments with the current implementation are promising. However, Knuth-Bendix procedure in the context of ML is a complex and new research problem and it needs a lot of work, for instance to handle proof in arithmetic which are often needed. Here is an example of a proof in arithmetic, checked in the current version, which is not completely satisfactory (because too hard to write), but shows the use of a language for both proofs and programs and the use of recursive functions for inductive proofs:

val rec mul_associative x y z |- (x * y) * z == x * (y * z)
  proof match x with
    Z[] -> 8< (* scissors meaning the end of a proof branch *)
  | S[x'] -> 
      let hr = mul_associative x' y z in
      let _ = mul_right_distributive y (x' * y) z in

Relation with ML language

The ML programming language, created by Robin Milner <em>et al</em> in the 80th has two major distinctive features:

  • Algebraic data-types and pattern matching: data types are basically all constructed using fixpoint, cartesian product (product types) and disjoint union (sum types).
  • Static type inference: the type of every piece of code is automatically inferred using Hindley-Milner algorithm (HM) and by construction, once compiled, an ML program can not crash (no segmentation fault). More precisely, when we do not use unsafe features of the language (like interface with unsafe libraries written in C), if an ML program crashes, then there is a bug in the type-checker or the compiler.

Recent progress in type inference algorithm uses constraint solving. This means that the type system can be described in first-order predicate logic in such a way that a type inference problem is a formula written in a decidable fragment of first-order predicate logic (often the purely existential fragment). Hence, any constraint solver can be turned into a type-check for ML. These approach is known as HM(X) (see [SOW97]).

There are two problems with this approach:

  • The complexity of constraint solving can be too high for practical use, especially using general purpose constraint solver. Currently (to our knowledge), there are no mainstream implementation of ML based on HM(X).
  • HM(X) does not completely solve all problems of subtyping. The language to express the types constructed by the algorithm is the same as the language used by programmers to write types. Hence, if we have the constraints <math>\alpha \subseteq \beta</math> and <math>\alpha \subseteq \gamma</math> for three types <math>\alpha, \beta</math> and <math>\gamma</math>, then the most natural solution would say that <math>\alpha = \beta \cap \gamma</math>. This implies that intersection of types needs to be part of the language for type. This means that constraints like <math>\beta \cap \gamma \subseteq \delta</math> may also appear and they are problematic to deal with. Moreover, the same reasoning apply for union and then, constraints of the form <math>\beta \cap \gamma \subseteq \beta' \cup \gamma'</math> may appear and at least increase a lot the complexity of constraint solving.

PML's approach is to replace type-inference by just constraint checking: we just check that a solution exists for the constraints in some model. The syntax to write the solution is not available to write types in the language and is even not defined. Type-checking in the current implementation of PML can be seen as a black box ensuring that nothing can go wrong during execution. Furthermore, the types used by the programmer are in fact only syntactic sugar for the projection operator onto the intended type (giving for free nice feature like higher-oder parametric types, that is types with parameters which may be themselves types with parameters).

With this approach, we loose type-inference and the ability to display types in error messages. Nevertheless, in case of error, we display three positions in the code and an error message like this <tt>error at position 1, label "id" projected at position 2 do not appear in the value constructed at position 3</tt>. This kind of error message is in fact of bounded length and often more useful than OCaml or SML messages. We can understand this as showing three points in the slice of the error, which is introduced by Joe Wells in [HW04]

Relation with existing proof assistants

Proof assistants have evolved rapidly since Automath in the 70th. Two main threads exist: automated proof assistants such as ACL2, PVS and safe ones such as Coq, Isabelle, PhoX, Lego, HOL, Matita, <em>etc.</em> The former incorporate very sophisticated automated deduction strategies, with no certificate for the validity of the proof, while the later require all proofs to be done in a specific framework (like natural deduction or type theory) allowing for a simple check of the proof. The gap between the two approaches tend to be reduced, by the emergence of complex tactics (for Coq or Isabelle mainly) that build proofs for you. For instance Zenon is an almost state of the art automated first-order theorem prover that outputs a Coq proof.

The common defect of all these proof assistants is that a proof can not be written nor understood without running the proof assistant. Some proof assistants do not follow exactly the above scheme: for instance Mizar and Alf. Mizar has a declarative style for proof which is humanly readable and checked by a limited checker (this proof style has been adapted to Coq and Isabelle). Unfortunately, there is no formal description of the Mizar proof checker. Alf on the other hand is based on proof theory and requires the user to basically write the complete proof tree just leaving out a few details. The logic is very well formalized and simple, but writing proof is tedious and not similar to usual practice in informal mathematics.

This pictures of the world of proof assistants shows that some fundamental work should be done here. In the current version of PML, the logic is just an equational theory of the underlying programming language which should be easy to describe formally when it is stabilized. And the proof engine is, like in Mizar, a limited automated checker inspired by the Knuth-Bendix completion algorithm (KB). But KB has to adapted to the higher-order constructs of ML-like languages and also to be limited to always terminate and possibly be fast. The current limitation is much too strong (it is limited to closed terms and can not use universal theorems automatically as in the second example of section 1 where one has to make precise how we use distributivity).

Nevertheless, examples in the current version shows that our approach is worth trying, because our first proofs are concise and readable (when you know the language). A very encouraging point is that all examples where written without interface. This really means that proofs are readable without the help of a computer.

Three "black boxes"


Termination criterion