> You've made an important and very common mistake of not qualifying this: it only holds true within the system.
It's not a mistake. I've stated it clearly.
You're effectively qualifying it by saying you can add more axioms to extend the mathematical system to render previously incomplete statements complete. This comes at the cost of adding more incomplete statements. I can add the "The Riemmann hypothesis is true" as an axiom, say, and, assuming it's consistent with other axioms and actually adds some power that other axioms didn't, that might be fine, but this will create other statements that are also incomplete.
> TLA+ and other "external" systems can evaluate whether a program has a bug.
No, it won't.
From the Wikipedia entry [0]:
> The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness.
From this, at best this only does it out to a finite number of execution steps. I suspect this comes at the cost of exponential resources. So not only does it not find all bugs, the bugs it does find come at an increasingly intractable cost.
It's not a mistake. I've stated it clearly.
You're effectively qualifying it by saying you can add more axioms to extend the mathematical system to render previously incomplete statements complete. This comes at the cost of adding more incomplete statements. I can add the "The Riemmann hypothesis is true" as an axiom, say, and, assuming it's consistent with other axioms and actually adds some power that other axioms didn't, that might be fine, but this will create other statements that are also incomplete.
> TLA+ and other "external" systems can evaluate whether a program has a bug.
No, it won't.
From the Wikipedia entry [0]:
> The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness.
From this, at best this only does it out to a finite number of execution steps. I suspect this comes at the cost of exponential resources. So not only does it not find all bugs, the bugs it does find come at an increasingly intractable cost.
[0] https://en.wikipedia.org/wiki/TLA%2B