Logic and Programming: From Algorithm to Verification

Program as a Logical Proof

Curry-Howard correspondence: programs and proofs are one and the same. A type in programming corresponds to a proposition in logic; a program implementing that type is a proof of that proposition. This is not a metaphor—it is a strict mathematical connection.

Consequence: programming languages with rich type systems (Haskell, Coq, Agda) allow logical constraints to be encoded directly in the code—so that an incorrect program simply will not compile. "The type system is the specification; the compiler is the verifier."

Formal program verification: a mathematical proof that a program meets its specification. Used in mission-critical systems: nuclear reactors, aviation, medical devices. In 2022, the CompCert compiler (a formally verified C compiler) was the first to obtain a formal proof of correctness—requiring 6 person-years of work.

Algorithmic Complexity and Practice

P vs. NP—the central open question in computer science. Practical consequences. Traveling Salesman Problem (TSP): for $n$ cities, find the shortest route. NP-complete problem—no known polynomial algorithm. For 1000 cities, brute force requires more operations than atoms in the universe. Heuristics are used: genetic algorithms, simulated annealing.

Quicksort algorithms—practically $O(n \log n)$, theoretically $O(n^2)$ in the worst case. Dijkstra’s algorithm—shortest path—$O(V^2)$ or $O(E \log V)$. These are pieces of knowledge that affect the performance of any IT system.

"No Free Lunch" theorem: there is no optimization algorithm that outperforms all others on every problem. An algorithm that is best for one class of problems is worse for another. This is a mathematically proven reason why a "universal" AI cannot exist.

Question for reflection: Algorithmic thinking is dividing a task into deterministic steps. Which tasks in your work can be algorithmized, and which require judgment that cannot be algorithmized?