3 ms·

> proofs for proofs. What does that even mean? Sorry, this is just a nonsensical term. The issue is not that the proofs could be wrong. It's that humans don't

> proofs for proofs. What does that even mean? Sorry, this is just a nonsensical term. The issue is not that the proofs could be wrong. It's that humans don't understand them even if they are verifibly correct. In contrast, with software you don't know if it's correct. That's what you have a test for. Even if you understand it, there could be a bug. And tests could have bugs too, so you can have tests for tests. But proofs that are verified are correct. That's it. Imagine you have a program that is formally proved to be correct. You don't need a test for it. However you might not understand it. Having a test or not does not change that. TL;DR: Correctness and understandability are (mostly) independent properties.

jdw64 4mo ago
[dead]
bananaflag 4mo ago
Thank you for spelling this in detail! One thing I might add is that not all programs can be proved to be correct for the simple reason that not all purposes of a program can be mathematically specified. For example, for (even "closed world" domain programs like) a chess engine, the one thing that matters (in the absence of a complete solution of a game like there exists in checkers) is "can beat world champions", which can only be tested empirically. Or sometimes, e.g. business logic software, the purpose can be mathematically specified but not in a simpler way than the code itself.
- skydhash 4mo ago
  It cannot be mathematically specified because there’s no way to formalize the statements. Also code is a mathematical object, but running code (the process) is not because it’s just electricity in metals and semiconductors. We modify the voltage somewhere and that leads to a transformation (light in displays, sound in speakers,..) somewhere else. We do have models for all of this but they are approximations, not the real representation.

jdw64 4mo ago

[dead]

bananaflag 4mo ago

Thank you for spelling this in detail! One thing I might add is that not all programs can be proved to be correct for the simple reason that not all purposes of a program can be mathematically specified. For example, for (even "closed world" domain programs like) a chess engine, the one thing that matters (in the absence of a complete solution of a game like there exists in checkers) is "can beat world champions", which can only be tested empirically. Or sometimes, e.g. business logic software, the purpose can be mathematically specified but not in a simpler way than the code itself.

skydhash 4mo ago
It cannot be mathematically specified because there’s no way to formalize the statements. Also code is a mathematical object, but running code (the process) is not because it’s just electricity in metals and semiconductors. We modify the voltage somewhere and that leads to a transformation (light in displays, sound in speakers,..) somewhere else. We do have models for all of this but they are approximations, not the real representation.