Re:Terence Tao, "Machine Assisted Proof" [video]
by munchler on Wednesday February 14, 2024 @08:18PM
(#39377971)
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!
[ Parent
| on HN ]
Re:Terence Tao, "Machine Assisted Proof" [video]
by zaik on Wednesday February 14, 2024 @11:43PM
(#39379197)
Using the Curry-Howard isomorphism my program shows there is a mapping from HTTP requests to HTTP responses!
Re:Terence Tao, "Machine Assisted Proof" [video]
by renonce on Thursday February 15, 2024 @12:50AM
(#39379564)
That’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