| Kommentar |
One of the most fundamental insights of computer science is the existence of mathematical problems that can be very simply and precisely stated, yet cannot be solved algorithmically.
This insight is part of a larger theory of computability, which is based upon the notion of recursive functions, or alternatively, Turing machines.
Knowing precisely if a function is (algorithmically) computable is valuable.
For example, in programming language design, introducing a new feature without knowing its computablity properties might break compiler termination.
Traditional computability theory relies on Gödel encodings, sometimes obscuring the underlying mathematical structure.
In contrast, synthetic computability theory assumes a mathematical universe in which functions transport computability.
This allows us to forgo Turing machines and focus on the actual mathematical objects, supported by a proof assistant (such as Coq). |
