4 ms·

Dumb question about contracts: I was reading the docs (https://c3-lang.org/language-common/contracts/ https://c3-lang.org/language-common/contracts/) and this j

Dumb question about contracts: I was reading the docs (https://c3-lang.org/language-common/contracts/ https://c3-lang.org/language-common/contracts/) and this jumped out "Contracts are optional pre- and post-condition checks that the compiler may use for static analysis, runtime checks and optimization. Note that conforming C3 compilers are not obliged to use pre- and post-conditions at all. However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated. In safe mode, pre- and post-conditions are checked using runtime asserts." So I'm probably missing something, but it reads to me like you're adding checks to your code, except there's no guarantee that they will run and whether it's at compile or runtime. And sometimes instead of catching a mistake, these checks will instead silently introduce undefined behaviour into your program. Isn't that kinda bad? How are you supposed to use this stuff reliably? (otherwise C3 seems really cool!)

pkulak 10mo ago
It seems to me like a way to standardize what happens all the time anyway. Compilers are always looking for ways to optimize, and that generally means making assumptions. Specifying those assumptions in the code, instead of in flags to the compiler, seems like a win.
riazrizvi 10mo ago
It’s giving you an expression capability so that you can state your intent, in a standardized way, that other tooling can build off. But it’s recognizing that the degree of enforcement depends on applied context. A big company team might want to enforce them rigidly, but a widely used tool like Visual Studio would not want to prevent code from running, so that folks who are introducing themselves to the paradigm can start to see how it would work, through warnings, while still being able to run code.
- SkiFire13 10mo ago
  This is not just expressing intent. The documentation clearly states that it's UB to violate them, so you need to be extra careful when using them.
  - riazrizvi 10mo ago
    Perhaps another helpful paradigm are traffic/construction cones with ‘do not cross’ messages. Sometimes nothing happens, other times you run into wet concrete, other times you get a ticket. They’re just plastic objects, easy to move, but you are not meant to cross them in your vehicle. While concrete bollards are a thing, they are only preferable in some situations.
    - SkiFire13 10mo ago
      I don't think this analogy fully respects the situation here. These pre/post condition are not just adding a warning to not do something, they also add a potentially bigger danger if they are broken. It's as if you also added a trap behind the construction cone which can do more damage than stepping on the wet concrete!
  - Phil_Latio 10mo ago
    > documentation clearly states that it's UB to violate them Only in "fast" mode. The developer has the choice: > Compilation has two modes: “safe” and “fast”. Safe mode will insert checks for out-of-bounds access, null-pointer deref, shifting by negative numbers, division by zero, violation of contracts and asserts.
    - SkiFire13 10mo ago
      > The developer has the choice The developer has the choice between fast or safe. They don't have a choice for checking pre/post conditions, or at least avoiding UB when they are broken, while getting the other benefits of the "fast" mode. And all in all the biggest issue is that these can be misinterpreted as a safety feature, while they actually add more possibilities for UB!
      - Phil_Latio 10mo ago
        Well, the C3 developer could add more fine grained control if people need it... I don't really see what's your problem. It's not so much different than disabling asserts in production. Some people don't do that, because they rather crash than walking into invalid program state - and that's fine too. It largely depends on the project in question.
Windeycastle 10mo ago
The way I reason about it is that the contracts are more soft conditions that you expect to not really reach. If something always has to be true, even on not-safe mode, you use "actual" code inside the function/macro to check that condition and fail in the desired way.
- cwillu 10mo ago
  “However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated” This implies that a compiler would be permitted to remove precisely that actual code that checks the condition in non-safe mode. Seems like a deliberately introduced footgun.
  - cloud-oak 10mo ago
    My understanding of this was that the UB starts only after the value is passed/returned. So if foo() has a contract to only return positive integers, the code within foo can check and ensure this, but if the calling code does it, the compiler might optimize it away.
    - gku 10mo ago
      Unspecified behavior != UB https://en.wikipedia.org/wiki/Unspecified_behavior https://en.wikipedia.org/wiki/Unspecified_behavior
    - cwillu 10mo ago
      Assuming that is correct, it's still exactly the same footgun. Checks like that are introduced to guard against bugs: you are strictly safer to not declare such a constraint.
- coldtea 10mo ago
  >The way I reason about it is that the contracts are more soft conditions that you expect to not really reach What's the difference from an assert then?
tialaramex 10mo ago
Contracts are a way to express invariants, "This shall always be true". There are three main things you could do with these invariants, the exact details of how to do them, and whether people should be allowed to specify which of these things to do, and if so whether they can pick only for a whole program, per-file, per-function, or whatever, is separate. 1. Ignore the invariants. You wrote them down, a human can read them, but the machine doesn't care. You might just as well use comments or annotate the documentation, and indeed some people do. 2. Check the invariants. If the invariant wasn't true then something went wrong and we might tell somebody about that. 3. Assume these invariants are always true. Therefore the optimiser may use them to emit machine code which is smaller or faster but only works if these invariants were correct. So for example maybe a language lets you say only that the whole program is checked, or, that the whole program can be assumed true, or, maybe the language lets you pick, function A's contract about pointer validity we're going to check at runtime, but function B's contract that you must pick an odd number, we will use assumption, we did tell you about that odd number requirement, have the optimiser emit that slightly faster machine code which doesn't work for N=0 -- because zero isn't an odd number assumption means it's now fine to use that code.
- ajuc 10mo ago
  So the compiler could have debug mode where it checks the invariants and release mode where it assumes they are true and optimizes around that without checking?
  - esrauch 10mo ago
    Yes, and that same pattern already does exist in C and C++. Asserts that are checked in debug builds but presumed true for optimization in release builds.
    - mananaysiempre 10mo ago
      Not unless you write your own assert macro using C23 unreachable(), GNU C __builtin_unreachable(), MSVC __assume(0), or the like. The standard one is defined[1] to either explicitly check or completely ignore its argument. [1] https://port70.net/~nsz/c/c11/n1570.html#7.2 https://port70.net/~nsz/c/c11/n1570.html#7.2
bluecalm 10mo ago
I think they are there to help the compiler so the optimizer might (but doesn't have to) assume they are true. It's sometimes very useful to be able to do so. For example if you know that two numbers are always different or that some value is always less than x. In standard C it's impossible to do but major compilers have a way to express it as extensions. GCC for example has: if (x) __builtin_unreachable(); C3 makes it a language construct. If you want runtime checks for safety you can use assert. The compiler turns those into asserts in safe/debug mode because that help catching bugs in non performance critical builds.
- florianist 10mo ago
  In the current C standard that's unreachable() from <stddef.h>
  - bluecalm 10mo ago
    Thank you, I've just recently read the list of new features and missed this one!
nomnomconflicts 10mo ago
- "Note that conforming C3 compilers are not obliged to use pre- and post-conditions at all." means a compiler doesn't have to use the conditions to select how the code will be compiled, or if there's a compile-time error. - "However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated." basically, it just states the obvious. the compler assumes a true condition is what the code is meant to address. it won't guess how to compile the code when the condition is false. - "In safe mode, pre- and post-conditions are checked using runtime asserts." it means that there's a 'mode' to activate the conditions during run-time analysis, which implies there's a mode to turn it off. this allows the conditions to stay in the source code without affecting runtime performance when compiled for production/release.
fuzztester 10mo ago
Design by contract is good. I've used it in some projects. https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract I first came across it when I was reading Bertrand Meyer's book, Object-oriented Software Construction. https://en.wikipedia.org/wiki/Object-Oriented_Software_Construction https://en.wikipedia.org/wiki/Object-Oriented_Software_Const... From the start of the article: [ Object-Oriented Software Construction, also called OOSC, is a book by Bertrand Meyer, widely considered a foundational text of object-oriented programming.[citation needed] The first edition was published in 1988; the second edition, extensively revised and expanded (more than 1300 pages), in 1997. Many translations are available including Dutch (first edition only), French (1+2), German (1), Italian (1), Japanese (1+2), Persian (1), Polish (2), Romanian (1), Russian (2), Serbian (2), and Spanish (2).[1] The book has been cited thousands of times. As of 15 December 2011, The Association for Computing Machinery's (ACM) Guide to Computing Literature counts 2,233 citations,[2] for the second edition alone in computer science journals and technical books; Google Scholar lists 7,305 citations. As of September 2006, the book is number 35 in the list of all-time most cited works (books, articles, etc.) in computer science literature, with 1,260 citations.[3] The book won a Jolt award in 1994.[4] The second edition is available online free.[5] ] https://en.wikipedia.org/wiki/Bertrand_Meyer https://en.wikipedia.org/wiki/Bertrand_Meyer

pkulak 10mo ago

It seems to me like a way to standardize what happens all the time anyway. Compilers are always looking for ways to optimize, and that generally means making assumptions. Specifying those assumptions in the code, instead of in flags to the compiler, seems like a win.

riazrizvi 10mo ago

It’s giving you an expression capability so that you can state your intent, in a standardized way, that other tooling can build off. But it’s recognizing that the degree of enforcement depends on applied context. A big company team might want to enforce them rigidly, but a widely used tool like Visual Studio would not want to prevent code from running, so that folks who are introducing themselves to the paradigm can start to see how it would work, through warnings, while still being able to run code.

SkiFire13 10mo ago
This is not just expressing intent. The documentation clearly states that it's UB to violate them, so you need to be extra careful when using them.
- riazrizvi 10mo ago
  Perhaps another helpful paradigm are traffic/construction cones with ‘do not cross’ messages. Sometimes nothing happens, other times you run into wet concrete, other times you get a ticket. They’re just plastic objects, easy to move, but you are not meant to cross them in your vehicle. While concrete bollards are a thing, they are only preferable in some situations.
  - SkiFire13 10mo ago
    I don't think this analogy fully respects the situation here. These pre/post condition are not just adding a warning to not do something, they also add a potentially bigger danger if they are broken. It's as if you also added a trap behind the construction cone which can do more damage than stepping on the wet concrete!
- Phil_Latio 10mo ago
  > documentation clearly states that it's UB to violate them Only in "fast" mode. The developer has the choice: > Compilation has two modes: “safe” and “fast”. Safe mode will insert checks for out-of-bounds access, null-pointer deref, shifting by negative numbers, division by zero, violation of contracts and asserts.
  - SkiFire13 10mo ago
    > The developer has the choice The developer has the choice between fast or safe. They don't have a choice for checking pre/post conditions, or at least avoiding UB when they are broken, while getting the other benefits of the "fast" mode. And all in all the biggest issue is that these can be misinterpreted as a safety feature, while they actually add more possibilities for UB!
    - Phil_Latio 10mo ago
      Well, the C3 developer could add more fine grained control if people need it... I don't really see what's your problem. It's not so much different than disabling asserts in production. Some people don't do that, because they rather crash than walking into invalid program state - and that's fine too. It largely depends on the project in question.

Windeycastle 10mo ago

The way I reason about it is that the contracts are more soft conditions that you expect to not really reach. If something always has to be true, even on not-safe mode, you use "actual" code inside the function/macro to check that condition and fail in the desired way.

cwillu 10mo ago
“However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated” This implies that a compiler would be permitted to remove precisely that actual code that checks the condition in non-safe mode. Seems like a deliberately introduced footgun.
- cloud-oak 10mo ago
  My understanding of this was that the UB starts only after the value is passed/returned. So if foo() has a contract to only return positive integers, the code within foo can check and ensure this, but if the calling code does it, the compiler might optimize it away.
  - gku 10mo ago
    Unspecified behavior != UB https://en.wikipedia.org/wiki/Unspecified_behavior https://en.wikipedia.org/wiki/Unspecified_behavior
  - cwillu 10mo ago
    Assuming that is correct, it's still exactly the same footgun. Checks like that are introduced to guard against bugs: you are strictly safer to not declare such a constraint.
coldtea 10mo ago
>The way I reason about it is that the contracts are more soft conditions that you expect to not really reach What's the difference from an assert then?

tialaramex 10mo ago

Contracts are a way to express invariants, "This shall always be true". There are three main things you could do with these invariants, the exact details of how to do them, and whether people should be allowed to specify which of these things to do, and if so whether they can pick only for a whole program, per-file, per-function, or whatever, is separate. 1. Ignore the invariants. You wrote them down, a human can read them, but the machine doesn't care. You might just as well use comments or annotate the documentation, and indeed some people do. 2. Check the invariants. If the invariant wasn't true then something went wrong and we might tell somebody about that. 3. Assume these invariants are always true. Therefore the optimiser may use them to emit machine code which is smaller or faster but only works if these invariants were correct. So for example maybe a language lets you say only that the whole program is checked, or, that the whole program can be assumed true, or, maybe the language lets you pick, function A's contract about pointer validity we're going to check at runtime, but function B's contract that you must pick an odd number, we will use assumption, we did tell you about that odd number requirement, have the optimiser emit that slightly faster machine code which doesn't work for N=0 -- because zero isn't an odd number assumption means it's now fine to use that code.

ajuc 10mo ago
So the compiler could have debug mode where it checks the invariants and release mode where it assumes they are true and optimizes around that without checking?
- esrauch 10mo ago
  Yes, and that same pattern already does exist in C and C++. Asserts that are checked in debug builds but presumed true for optimization in release builds.
  - mananaysiempre 10mo ago
    Not unless you write your own assert macro using C23 unreachable(), GNU C __builtin_unreachable(), MSVC __assume(0), or the like. The standard one is defined[1] to either explicitly check or completely ignore its argument. [1] https://port70.net/~nsz/c/c11/n1570.html#7.2 https://port70.net/~nsz/c/c11/n1570.html#7.2

bluecalm 10mo ago

I think they are there to help the compiler so the optimizer might (but doesn't have to) assume they are true. It's sometimes very useful to be able to do so. For example if you know that two numbers are always different or that some value is always less than x. In standard C it's impossible to do but major compilers have a way to express it as extensions. GCC for example has: if (x) __builtin_unreachable(); C3 makes it a language construct. If you want runtime checks for safety you can use assert. The compiler turns those into asserts in safe/debug mode because that help catching bugs in non performance critical builds.

florianist 10mo ago
In the current C standard that's unreachable() from <stddef.h>
- bluecalm 10mo ago
  Thank you, I've just recently read the list of new features and missed this one!

nomnomconflicts 10mo ago

- "Note that conforming C3 compilers are not obliged to use pre- and post-conditions at all." means a compiler doesn't have to use the conditions to select how the code will be compiled, or if there's a compile-time error. - "However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated." basically, it just states the obvious. the compler assumes a true condition is what the code is meant to address. it won't guess how to compile the code when the condition is false. - "In safe mode, pre- and post-conditions are checked using runtime asserts." it means that there's a 'mode' to activate the conditions during run-time analysis, which implies there's a mode to turn it off. this allows the conditions to stay in the source code without affecting runtime performance when compiled for production/release.

fuzztester 10mo ago

Design by contract is good. I've used it in some projects. https://en.wikipedia.org/wiki/Design_by_contract https://en.wikipedia.org/wiki/Design_by_contract I first came across it when I was reading Bertrand Meyer's book, Object-oriented Software Construction. https://en.wikipedia.org/wiki/Object-Oriented_Software_Construction https://en.wikipedia.org/wiki/Object-Oriented_Software_Const... From the start of the article: [ Object-Oriented Software Construction, also called OOSC, is a book by Bertrand Meyer, widely considered a foundational text of object-oriented programming.[citation needed] The first edition was published in 1988; the second edition, extensively revised and expanded (more than 1300 pages), in 1997. Many translations are available including Dutch (first edition only), French (1+2), German (1), Italian (1), Japanese (1+2), Persian (1), Polish (2), Romanian (1), Russian (2), Serbian (2), and Spanish (2).[1] The book has been cited thousands of times. As of 15 December 2011, The Association for Computing Machinery's (ACM) Guide to Computing Literature counts 2,233 citations,[2] for the second edition alone in computer science journals and technical books; Google Scholar lists 7,305 citations. As of September 2006, the book is number 35 in the list of all-time most cited works (books, articles, etc.) in computer science literature, with 1,260 citations.[3] The book won a Jolt award in 1994.[4] The second edition is available online free.[5] ] https://en.wikipedia.org/wiki/Bertrand_Meyer https://en.wikipedia.org/wiki/Bertrand_Meyer