3 ms·
Theorem provers like Lean are awesome. As a software guy who admires mathematics from a safe distance, the Curry-Howard isomorphism is one of the most beautiful
by munchler 3y ago
Theorem provers like Lean are awesome. As a software guy who admires mathematics from a safe distance, the Curry-Howard isomorphism is one of the most beautiful and surprising things I've ever seen. Programs are proofs!
- zaik 3y agoUsing the Curry-Howard isomorphism my program shows there is a mapping from HTTP requests to HTTP responses!
- renonce 3y agoThat’s far off, your program also branches to standard libraries and kernel syscalls and networking with other servers and maybe loops that aren’t guaranteed to terminate, that there are 10000s of cases where HTTP requests map to an error (bottom) instead of a response