We care only about a very small and narrow subset of possible programs, not any ...

		mkl 19 days ago \| parent \| context \| favorite \| on: Lean proved this program correct; then I found a b... 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.