3 ms·
OK, but that's a reactor control system. If your application has no time-critical aspect, is there any good reason to prefer a proof over an assert?
by 0xDEAFBEAD 1y ago
OK, but that's a reactor control system. If your application has no time-critical aspect, is there any good reason to prefer a proof over an assert?
- dbdr 1y agoWill your users be happier to get an assertion failure when they run your code, compared to no error? (the tradeoff of course being that they might get your code later because it took more time to prove the code is correct)
- 0xDEAFBEAD 1y agoWhat if it's an internal tool, where correctness matters a lot, but failures matter little? E.g. roll back all database changes in case of assertion failure. Perhaps an accounting thing or something of that nature.
- addaon 1y agoIf your application has no time-critical aspect, why are you working on it now? There’s plenty of time to get to it later.
- 0xDEAFBEAD 1y agoVery funny!
- empath75 1y agoBecause a run-time error produces a failure at runtime or a crash. You would much prefer that errors are impossible.
- epolanski 1y agoYes, a proof allows me to not have to handle the case at all.