3 ms·
No, the correctness of your implementation is a mathematical statement about a computation running a particular computational environment, and can be reasoned a
by Ar-Curunir 1y ago
No, the correctness of your implementation is a mathematical statement about a computation running a particular computational environment, and can be reasoned about from first principles without ever invoking a computer. Whether your computation gives reasonable outputs on certain inputs says nothing (in general) about the original mathematics.
- falcor84 1y agoWhile mathematics "can" be reasoned about from first principles, the history of math is chock-full of examples of professional mathematicians convinced by unsound and wrong arguments. I prefer the clarity of performing math experiments and validating proofs on a computer.
- Ar-Curunir 1y agoYes, but a C or Python program that “implements” a proof and which you test by running it on a few inputs is very different from a program in a interactive theorem prover like Rocq or Lean. In the latter, validity is essentially decided by type-checking, not execution