Constructing a Calculus of Programs

A large part of the effort in formal program developments i expended on repeating the same derivational patterns over and over again. The problem is compounded by notations that require many marks on paper for expressing one elementary concept, and 'administrative overhead', consisting of atgorithmicatly uninteresting but technically necessary steps, like shuffling parts of an expression around without change in computational meaning, and the introduction of local auxiliary definitions for lack of a suitable notation for what is being defined. This can to a large extent be avoided by developing suitable theories, including a notation that is designed to increase the manipulability. After a reflexion on some of the issues, the more technical part of this paper is devoted to an attempt o construct a system of combinators that is better amenable to manipulation than the classical ones. Program construction is a mathematical ctivity. By 'mathematical ctivity ' is not meant: the actual practice of professional mathematicians, but: establishing proper-ties of formal objects with perfect certainty, that is, as a tautology. Often the pro-perty to be estabfished is known, but the formal object that has to enjoy the pro