>properties like all x in Int: inc(x) > x.

Why not just use an assertion? It costs more at runtime, but it's far less dev time than developing a proof, right?

▲ kryptiskt 8 hours ago | parent | next [-]

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 6 hours ago | parent [-]

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 6 hours ago | parent | next [-]

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)

	▲	0xDEAFBEAD 5 hours ago \| parent [-]
		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.

▲

addaon 5 hours ago | parent | prev | next [-]

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.

	▲	0xDEAFBEAD 5 hours ago \| parent [-]
		Very funny!

▲

empath75 21 minutes ago | parent | prev [-]

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

▲ mrkeen 8 hours ago | parent | prev | next [-]

Nearly everything that goes wrong for me in prod is already a crash/stacktrace, which is what an assertion does.

The point of proofs is to not get yourself (or the customer) into that point in the first place.

▲ djoldman 3 hours ago | parent | prev | next [-]

I think other responses here may miss an important line of thought.

There seems to be confusion around the differences between bug and correct.

In the referenced study on binary searches, the Google researchers stated that most implementations had bugs AND were "broken" because they did:

    int mid =(low + high) / 2;

And low + high can overflow.

Ostensibly, a proof may require mid to be positive at all times and therefore be invalid because of overflow.

The question is: if we put in assertions everywhere that guarantee correct output, where aborting on overflow is considered correct, then are folks going to say that's correct, or are they going to say oh that's not what binary search is so you haven't implemented it?

EDIT: thinking about it more, it seems that null must be an accepted output of any program due to the impossibility of representing very large numbers.

▲ hshdhdhehd 4 hours ago | parent | prev | next [-]

Correct. You wouldn't prove everything in a typical production system unless that system is controlling a rocket or a pacemaker.

You may want to prove some things. Test others.

Types are proofs by the way. Most programmers find that handy.

I think assertions are rediculously underused BTW

▲ rwmj 4 hours ago | parent | prev | next [-]

If you're flying a plane, you probably don't want safety critical code to throw an assertion. It's for this reason that Airbus spends a bunch of money & time on proving their flight control software.

▲ AdieuToLogic 7 hours ago | parent | prev [-]

Better to use a type which cannot represent an invalid state.

For example, instead of defining `inc` with `Int`s, the equivalent of an `IncrementalInt` type parameter for the `inc` function will ensure correctness without requiring runtime assertions.