3 ms·
All we need now is a proof that the proof program is correct. And a proof that the proof proving program is correct.
by TwoBit 10y ago
All we need now is a proof that the proof program is correct. And a proof that the proof proving program is correct.
- pka 10y agoExactly :) And a proof that the spec is correct. But without formal verification both your spec and the implementation may be incorrect.
- AstralStorm 10y agoInternal consistency is relatively easy to verify. Completeness to some extent as well. The manual task is to verify all the assumptions.