How Does Mathematics Relate to the Design of a Software?

In a recent article from Quanta Magazine, titled “How to Write Software with Mathematical Perfection”, the interviewee Turing Award laureate Leslie Lamport suggests thinking about programs via mathematics. His thought does not come from nowhere; the origin of computer science is interconnected with a branch of mathematics called constructive mathematics.

In constructive mathematics, a task that could be performed by an algorithm is referred to as a computable function, which is defined as:

If the function is defined for input then the algorithm halts on the input and prints the output;

If the function is undefined, then the algorithm does not halt on the input.

The entire branch of constructive mathematics stretches surrounding the notion of a computable function, extending to properties such as decidability and enumerability. Part of it runs in parallel with mathematical analysis, which reorganizes the basics of mathematics in the modern and contemporary study of higher mathematics.

Constructive mathematics emerges before the Turing machines and computers, in fact, the study inspires the creations of Turing machines and computers. Rather than thinking of an algorithm in the fashion of pseudocodes or a programming language, constructive mathematics does not consider the specifics of an algorithm but ideally assumes its existence. The theorems in constructive mathematics provide a holistic view of an algorithm or the possibility of a task, which as said by Lamport, could facilitate the creation of a computer program.