Mathematical logic played an important role in the emergence of computers, although it was not the sole driving force in this complex process. It was in mathematical logic, in an attempt to give the most general definition of a problem with an algorithmic solution, that it was realized that it was possible to build a universal computing device (machine) that would be able to solve all theoretically solvable algorithmic problems.

One of the first to realize this was Alan Turing, who gave a precise definition and the most convincing analysis of the concept of a computable function in 1936. Other scientists who, along with Turing, came up with the same ideas around the same time were Alonzo Church and Emile Post. These and other researchers in the 1930s created the beginnings of algorithm theory, which became the basis for understanding the operation and construction of computing devices in the 40s and 50s. In particular, the idea of the universal Turing machine was later technically realized in the “von Neumann” computer architecture, according to which the program is stored in the memory of the device and can be modified during its operation. All operating systems are based on this idea.

The problem that the pioneers of algorithm theory sought to solve was the question posed by Hilbert, which he called in German Entscheidungsproblem, “the solution problem. The question was to find an algorithm that, for a given statement written in the language of predicate logic, would answer whether or not there was a formal proof of that statement. If such an algorithm existed, then all mathematical problems would, in a sense, have a purely mechanical solution: as mentioned above, almost any mathematical statement can be formulated in the language of predicate logic, such as the famous hypothesis about the infinity of the number of pairs of prime twin numbers. Then the question of whether this hypothesis is deducible from the axioms of set theory would be reduced to checking the provability of some statement in predicate calculus. Not surprisingly, the researchers of the Entscheidungsproblem sought to show that the required algorithm could not exist in principle.

If it is possible to prove the existence of a particular algorithm by presenting it explicitly, in order to argue that such an algorithm does not exist, it is necessary to have an exact mathematical description of the class of problems that admit an algorithmic solution. The answer to this question required the development of formal languages to describe algorithms even before computers appeared. Moreover, since the goal of such development was more theoretical than practical, researchers sought to formulate the simplest for description and at the same time universal computational models. The first such models were Gödel-Erbrand recursive functions, Church lambda calculus and Turing machines.

Gödel, though he was the first to actually formulate a universal programming language, did not believe that the concept he (and the French logician Erbrand) found was universal in the sense of being able to program any algorithm. Alonzo Church was the first to make a thesis about the universality of his computational model. He also presented a proof of the impossibility of solving the Entscheidungsproblem within this model. Church’s calculus was very simple in form, but it looked more like a formal logical calculus than a real computing machine. Turing machines were in this sense closer to future reality, and it was much easier to believe Turing’s thesis that any problem with an algorithmic solution could be solved by a Turing machine than a similar thesis by Church (Turing’s work is known to have convinced Gödel of the validity of this thesis). Turing also showed that his machines were equivalent to lambda-calculus in terms of computational capability, which was indirect evidence for the validity of the Church-Turing thesis, as it is now commonly called.

Subsequently, many researchers proposed their own computational models in the hope of extending the class of computable functions first described by Church and Turing. All such attempts failed to expand this class, which turned out to be very stable. Today, the Church-Turing thesis–understood in the sense of any of the equivalent computational models–is one of the cornerstones on which algorithm theory is based.

As for lambda-calculus, it has long been on the margins of mathematical logic, being displaced from the theory of algorithms by more convenient and intuitive models. However, in the second half of XX century lambda-calculus and systems based on it have found serious practical applications. Lambda-calculus has become a prototype of so called functional programming languages (such as the modern Haskell language), which have a number of advantages over traditional imperative languages and are now very actively developing.