Re:Lean proved this program correct; then I found a bug
by mkl on Monday April 13, 2026 @09:40PM
(#47760242)
We care only about a very small and narrow subset of possible programs, not any arbitrary one. It's possible to solve this kind of problem in large enough classes of program to be useful.
[ Parent
| on HN ]
There are no comments on this comment yet.