1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
#+title: Coq is cool
#+date: <2022-01-06>
Having written emacs lisp for a while and grown my emacs init file to thousands of lines, I decided to revisit the /[[http://landoflisp.com/][Land of Lisp]]/, a fanstastically and humorously written book about lisp.
The book said that lisp is basically lambda calculus, which got me thinking. How is it lambda calculus?
So I went back into the rabbit hole that drew me in a few years ago, not knowing that's where I was going. I started by refreshing my knowledge reading /[[https://www.cis.upenn.edu/~bcpierce/tapl/][Types and Programming Languages]]/ (TAPL). After reading it I still didn't quite get how lisp is basically lambda calculus.
TAPL mentioned Curry-Howard correspondence, a theory that connects logic systems with type systems. I wanted to know what each of the 8 vertices of the [[https://en.wikipedia.org/wiki/Lambda_cube][lambda cube]] corresponds to and how, which was not covered in TAPL. After a failed web surfing session in an attempt to find quick answers to my question, I was reminded of the /[[https://softwarefoundations.cis.upenn.edu/][Software Foundations]]/ series, and indeed, it talked about Curry-Howard correspondence with real code.
So I went on to read the first volume titled /[[https://softwarefoundations.cis.upenn.edu/lf-current/index.html][Logic Foundations]]/. Previously I had an (irrational?) aversion towards logic, fearing much of it was all dry tautology and not as fun as more "useful" mathematics like probably theory. Boy was I wrong. /Logic Foundations/ introduces coq, which I didn't touch due to the same aversion. But as it turned out, coq answered most of my questions about formal mathematics, and fully developed my (unoriginal) [[https://toywiki.xyz/][ideas of formalising mathematics]]. Maths is code. Theorems are identified by their proofs. You can apply a theorem in the proof of another theorem, matching terms. You can parameterise theorems etc. etc. Coq is something I wish I knew when I was a PhD student. The logic system is constrained in CoC, calculus of constructions, which is the top vertex in the lambda cube. I am still reading the book and can't wait to find out the extent of mathematics covered by it and what can be done about non-constructive systems (like the classical maths where you can cheat with excluded middle) using coq or other formal systems.
If one day programs and proofs are indistinguishable, the two traditions will blend. Maths has no copyright, but advanced maths can be hard to understand, though written in well-commented code it will be more accessible. Computer programs are the opposite, heavily copyrighted under good free licenses like (A)GPLv3+ and evil proprietary licenses, but more accessible (though code obfuscation is also thing but it cannot have gaps). My hope is this will bring the best of both worlds, that is, an elimination of copyright in computer programs (look, it is all maths, and copyrighting theorems and proofs are absurd!), and a more accessible corpus of advanced mathematics.
|
