*Programming with Theorem-Proving* (PwTP) is a rich and broad
programming paradigm that allows cohesive construction of programs and
proofs in a syntactically intwined manner. The support for PwTP in ATS is a
signatory feature of ATS, and the novelty of ATS largely stems from it. For
people who are familiar with the so-called Curry-Howard isomorphism, I
emphasize that PwTP as is supported in ATS makes little, if any, essential
use of this isomorphism (between proofs and programs): The dynamics of ATS
in which programs are written is certainly not pure and the proofs encoded
in ATS/LF are not required to be constructive, either. However, that proof
construction in ATS can be done in a style of (functional) programming is
fundamentally important in terms of syntax design for ATS, for the need to
combine programs with proofs would otherwise be greatly more challenging.

In this chapter, I will present some simple but convincing examples to illustrate the power and flexibility of PwTP as is supported in ATS. However, the real showcase for PwTP will not arrive until after the introduction of linear types in ATS, when linear proofs can be combined with programs to track and safely manipulate resources such as memory and objects (e.g, file handles). In particular, PwTP is to form the cornersone of the support for imperative programming in ATS.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

The constraint-solver of ATS is of rather diminished power. In particular, constraints containing nonlinear integer terms (e.g., those involving the use of multiplication (of variables)) are immediately rejected. This weakness must be properly addressed for otherwise it would become a crippling limitation on practicality of the type system of ATS. I now use a simple example to demonstrate how theorem-proving can be employed to circumvent the need for handling nonlinear constraints directly.

A function template list_concat is implemented as follows:

// // [list_concat] does typecheck in ATS2 // [list_concat] does not typecheck in ATS1 // fun{ a:t@ype } list_concat{m,n:nat} ( xss: list (list (a, n), m) ) : list (a, m * n) = case+ xss of | list_nil () => list_nil () | list_cons (xs, xss) => list_append<a> (xs, list_concat xss) // end of [list_concat]

fun{ a:t@ype } list_concat{m,n:nat} ( xss: list(list(a, n), m) ) : [p:nat] (MUL(m, n, p) | list(a, p)) = ( // case+ xss of | list_nil () => (MULbas() | list_nil()) | list_cons (xs, xss) => let val (pf | res) = list_concat (xss) in (MULind pf | list_append<a> (xs, res)) end // end of [list_cons] // ) (* end of [list_concat] *)