  We present the PML 2 language, which provides a uniform environment for
programming, and for proving properties of programs in an ML-like setting. The
language is Curry-style and call-by-value, it provides a control operator
(interpreted in terms of classical logic), it supports general recursion and a
very general form of (implicit, non-coercive) subtyping. In the system,
equational properties of programs are expressed using two new type formers, and
they are proved by constructing terminating programs. Although proofs rely
heavily on equational reasoning, equalities are exclusively managed by the
type-checker. This means that the user only has to choose which equality to
use, and not where to use it, as is usually done in mathematical proofs. In the
system, writing proofs mostly amounts to applying lemmas (possibly recursive
function calls), and to perform case analyses (pattern matchings).
