💾 Archived View for midnight.pub › replies › 7787 captured on 2024-08-18 at 21:40:14. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2024-03-21)
-=-=-=-=-=-=-
< Being a programmer in a world with fewer computers
Programming without a computer
This is called Mathematics, we've been doing it for 2000 years already, long before computers, and got pretty good at it :)
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
The Curry Howard correspondence is an equivalence between programming (specially functional programming) and proving theorems. This is not only a theoretical one, but proof assistants (a program to formally verify theorems) actually use it! LEAN started as a proof assistant (and was very slow) and now it is also a general purpose functional programming language. They even use it to program robots
https://galois.com/blog/2021/03/real-time-robotics-control-in-the-lean-language/