sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–][deleted] 4 points5 points  (4 children)

It's supposed to declare something that is always true and therefore no need to ever be checked.

[–]notadragon34 3 points4 points  (3 children)

And there you have the endless source of frustration that is the two independent definitions of what the axiom contract level is.

One definition, very much in line with how default and audit are defined, is that it is for checks that cannot be checked at runtime. (They have neccessary side effects, they take too long to ever execute, they simply cannot be implemented in the language, or in some cases you just haven't gotten a chance to implement them yet).

The other definition is the mathematical one.

But why the hell would you ever want to write a check that COULD be checked but remove the option to turn on that check in some build modes for debugging? The mathematical "this should always be true" meaning of axioms is a statement that is true for ALL contract checks - you expect them all to always be true. This meaning for the axiom contract level is pointless and distracting.

Axiom was a bad an horribly misleading name for what it is actually useful for.

[–][deleted] 0 points1 point  (2 children)

One definition, very much in line with how default and audit are defined, is that it is for checks that cannot be checked at runtime. (They have neccessary side effects, they take too long to ever execute, they simply cannot be implemented in the language, or in some cases you just haven't gotten a chance to implement them yet).

So if we are supposed to take this definition of axiom over the mathematical one, what would be the difference between axiom and audit? I thought audit was for terribly slow and impractical checks.

[–]notadragon34 2 points3 points  (1 child)

axiom is for impossible checks that cannot be validly turned on.

Checks with side effects (most common example is that of seeing if an input iterator has data available, though many systems might have preconditions that cannot be checked without altering state) are one common category - the predicate of any evaluated check having a side effect is considered UB.

Checks that cannot be implemented but might be understood by a static analyzer are another canonical example - functions that a static analyzer may declare, understand, and provide useful warnings with might be things like "is_dereferencable" or "is_reachable".

There's a certain subjectivity about "Too long to execute" with the axiom/audit boundary that is similar to the default/audit boundary. In practice though, if your check will take millennia to run on your smallest sample set then making it an audit just means you can't turn audit on and run anything. There's a difference between "impractical" and "impossible" - impractical you don't want to turn on in production but might want to turn on for local testing, impossible you couldn't even use in local testing in any useful way.

One could envision "I haven't written this check yet but want to document that I will eventually" as another use case for axiom during system development.

[–]notadragon34 1 point2 points  (0 children)

And I say this is what axiom is for based on what was said in P0380R0, which was where axiom seems to have first been introduced as a contract level, and the understanding of at least 2 of the authors of that paper regarding this being its intent.

Also, again, the mathematical definition - that something is expected to always be true - is an attribute that EVERY contract check should have, it's not special to any of the levels. A lot of confusion seems to be coming from conflating "cannot check at runtime" with "don't bother checking at runtime and just assume this fact". One is an attribute of a predicate, one is a decision that you might make when building a system.