Comment by kryptiskt

Comment by kryptiskt a day ago

7 replies

View on Hacker News

It's not a substitute, an assertion only makes sure that it doesn't happen unnoticed, a proof says that it doesn't happen at all. I might prefer to know that my reactor control system has no overflow ahead of time, rather than getting an assertion and crashing if it happens (though it would be a bad reactor control system if it couldn't handle crashes).

0xDEAFBEAD a day 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?

Reply View 6 replies
  • dbdr 21 hours ago

    Will 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)

    Reply View 1 reply
    • 0xDEAFBEAD 21 hours ago

      What 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.

      Reply View 0 replies
  • addaon 21 hours ago

    If your application has no time-critical aspect, why are you working on it now? There’s plenty of time to get to it later.

    Reply View 1 reply
  • epolanski 15 hours ago

    Yes, a proof allows me to not have to handle the case at all.

    Reply View 0 replies
  • empath75 16 hours ago

    Because a run-time error produces a failure at runtime or a crash. You would much prefer that errors are impossible.

    Reply View 0 replies