|
|
|
|
|
|
by xelxebar
2 days ago
|
|
|
Programs as data. Proofs of incompleteness theorems, the halting problem, Rice's theorem etc. all share a diagonalization structure. The keyword here is Lawvere's fixed-point theorem[0], but it's a bit of abstract nonsense, so here's a good accessible video on the topic[1]. I'm not sure the incompleteness theorems themselves are immediately and directly applicable to software development, but I find that having several examples of diagonaization proofs bouncing around in my head makes the Lawvere structure apparent. Since proofs are just programs, the pattern is surprisingly pervasive. Futamura projections are one incarnation, which is essentially how many interpreters end up providing "compilation" of programs into standalone binaries. [0]:https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theore... [1]:https://www.youtube.com/watch?v=dwNxVpbEVcc |
|
|