@y e List(A) (Perm(x,y) & Sorted(y)) which is read “for all lists x, there is a sorted permutation y of x”. We can prove that this proposition is true, using the rules of the language to construct a program for the task. If the proposition were not true, it would be impossible to find a program for it and we would have had an impossible task. The types of Constructive Set Theory can be seen as a specification language for the programs, but of course there is only one language, avoiding the complexity of mixing a programming language with a logical language.The similarity (or rather: identity) between a mathematical proof of a given proposition and a program for a given task suggests that programming should be similar to the mathematicians activity of finding proofs. We have illustrate d this with an example of how a proof of the Euclidean division theorem yields a program to compute the quotient and the remainder between two natural numbers.The paper contains a description of the language. Since all programs in the language terminate, the proof rules and the semantics are simple. We give some examples of programming with lists and reasoning about the programs. We also define the Ackermann function.