10 ms·

Contracts for C

108 points by joexbayer 1y ago

__d 1y ago
I like Eiffel. But if I want to use Eiffel, I’ll use Eiffel (or Sather). I’d rather C remained C. Maybe that’s just me?
- jimbob45 1y ago
  Java 24 and C# 9 resemble little of their first versions. C++ might as well not even be the same language at this point. Why are we so conservative with C but then so happily liberal with every other language?
  - dmitrygr 1y ago
    Because there must be at least one refuge for the sane
  - HexDecOctBin 1y ago
    People chose C because they liked C. Of course they don't want C to change. The only thing the ISO committee should be adding is stuff for filling in the holes in language (C23's Improved Tag Compatibility and __VA_OPT__ are good examples), not add features that were never part of C and were never supposed to be there. Your question can be reflected back to you: if you want an ever changing languages, go to Java, C# or C++, why mess with C?
    - xboxnolifes 1y ago
      > People chose C because they liked C. Of course they don't want C to change. The same thing can be said for every other language, yet they change.
      - oguz-ismail 1y ago
        Well they shouldn't have. It was much more fun to program in Python 2.7 and Java 7, I wouldn't touch those languages with a five feet pole these days
        lifthrasiir 1y ago
        Why specifically Python 2.7 and not, like, 1.5? Python 1 and 2 are as different as 2 and 3 (that is, surprisingly not much).
      - WalterBright 1y ago
        A common thing people write about D is don't add any more features except for their feature proposals. :-)
    - brabel 1y ago
      This is funny because Java people say the same about Kotlin and Scala.
    - pjmlp 1y ago
      No, many people chose C, because they had to.
      - sarchertech 1y ago
        Yeah but those people are running it on some platform where it’s the only choice. And they are probably running a subset of C99. The likelihood of new features ever making it to those platforms is close to zero.
        pjmlp 1y ago
        There is hardly any new C compiler that isn't C11.
        sarchertech 1y ago
        I’ve been out of embedded for a bit but last I checked almost nothing actually implemented all of C11?
        pjmlp 1y ago
        There is hardly any compiler worth using that isn't a fork of either GCC or clang. So unless they are stuck on a pre-historic fork, they support C11 as much as clang and GCC do. Exception for stuff like PIC, Z80,... Which didn't even support proper C on their glory days.
    - WalterBright 1y ago
      C added the absurd normalized Unicode identifiers.
  - nananana9 1y ago
    The complexity of C# and C++ should be a warning, not something to strive towards. C++ has 3 reasonable implementations, C has hundreds, for all sorts of platforms, where you don't get anything else. Most C developers don't want a modern C, they want a reliable C. WG14 should be pushing for clarifications on UB, the memory and threading model, documenting where implementations differ, and what parts of the language can be relied and what not. Nobody really needs a new way to do asserts, case ranges, or a new way to write the word "NULL".
    - lifthrasiir 1y ago
      C++ historically had much more implementations. It is probably more about the availability of quality compilers that are free to use and adapt, because even in C most new compilers for niche platforms are now based on GCC or clang for the practical reason.
      - pjmlp 1y ago
        Both implementated in C++. As someone that remembers the t-shirts with "my compiler compiles yours" that some C folks used to wear, it is kind of ironic having that turned around on them.
    - motorest 1y ago
      > The complexity of C# and C++ should be a warning, not something to strive towards. I think this talk about "complexity" is a red herring. C++ remains one of the most popular languages ever designed, and one of the key reasons is that since C++11 the standardization effort picked up steam and started including features that the developer community wanted and was eager to get. I still recall the time that randos criticized C++ for being a dead language and being too minimalistic and spartan. > C++ has 3 reasonable implementations, C has hundreds, for all sorts of platforms, where you don't get anything else. I don't understand what point you are trying to make. Go through the list of the most popular programming languages, and perhaps half of them are languages which only have a single implementation. What compelled you to criticize C++ for having at least 3 production-quality implementations? > Most C developers don't want a modern C, they want a reliable C. You speak only for yourself. Your personal opinion is based on survivorship bias. I can tel you that as a matter of fact a key reason why the likes of Rust took off was that people working with low-level systems programming were desperate for a C with better developer experience and sane and usable standard library. > Nobody really needs a new way to do asserts, case ranges, or a new way to write the word "NULL". Again, you speak for yourself, and yourself alone. You believe you don't need new features. That's fine. But you speak for yourself.
- OCTAGRAM 1y ago
  Eiffel has unsolicited tracing garbage collection. For TGC-free programming there is Ada
- veltas 1y ago
  Truly I agree, but if we can add features to improve C codebases without rewriting them then that's a win, and you can just ignore them if you don't like them (as I will), but to the people where this has benefit they can be used.
- pjmlp 1y ago
  Languages are software products like everything else in computing, either they evolve or they whither and die. C especially was designed with lots of security defects, and had it not been for UNIX being available for free, it would probably never taken off.
  - HexDecOctBin 1y ago
    More likely they evolve AND they whither and die. The number of software I have stopped using due to bad updates is much higher than those with not enough updates.
- johnisgood 1y ago
  Ada / SPARK has contracts, too, that can be proven at compile-time. In fact, Ada alone suffices, it has pre- and post-conditions. I think Ada has more libraries than Eiffel does. Does anyone even write Eiffel? I am really curious if it is still alive anywhere, in some form.
  - WalterBright 1y ago
    Eiffel failed largely because of licensing restrictions.
- flykespice 1y ago
  Are you being really honest with yourself that you would renounce c90, c99 additions to stay with the original language as it was introduced in K&R C book?
WalterBright 1y ago
Digital Mars C++ has had contracts since, oh, the early 1990s? https://www.digitalmars.com/ctg/contract.html https://www.digitalmars.com/ctg/contract.html
- motorest 1y ago
  > Digital Mars C++ has had contracts since, oh, the early 1990s? I think that implementations trying out their own experimental features is normal and expected. Ideally, standards would be pull-based instead of push-based. The real question is what prevented this feature from being proposed to the standardization committee.
  - arunc 1y ago
    It was proposed by Walter and denied by Stroustroup, probably to save C++. Karma hits back and he is trying to save C++ from Rust.
    - pjmlp 1y ago
      People keep forgetting C++ design is driven by 300+ people, and the features that get into the language go to elections, that they have to win. Stroustoup has one vote, not everything he advocates for wins votes, including having a saner C++ (Remember the Vasa paper).
    - motorest 1y ago
      > It was proposed by Walter and denied by Stroustroup, probably to save C++. Citation needed. For starters, where is the paper?
      - shakna 1y ago
        Well, there's this list Stroustrup offers, of systems in C++ that he would reject: [0] [0] https://open-std.org/JTC1/SC22/WG21/docs/papers/2018/p0977r0.pdf https://open-std.org/JTC1/SC22/WG21/docs/papers/2018/p0977r0...
taminka 1y ago
do i understand correctly that there's nothing preventing someone from adding a postcondition check X and then just not implementing it inside the function? wouldn't this just mean that now the ub is triggered by the post()'s `unceachable()` instead of whatever ub would happen w/, say, dereferencing a null pointer, as a consequence of not actually implementing post check X? so it's just for speed optimisations then? from reading about contracts for C before i assumed it would be like what cake[1] does, which actually compile time enforces pointer (non)nullability, as well as resource ownership and a bunch of other stuff, very cool project, check it out if you haven't seen it yet :) [1]https://github.com/thradams/cake https://github.com/thradams/cake
AlotOfReading 1y ago
There's a bit of an impedence mismatch with Contracts in C because C++ contracts exist partially to rectify the fact that <cassert> is broken in C++. Let's say you have a header lib.h: inline int foo(int i) { assert(i > 0); //... } In C, this function is unspecified behavior that will probably work if the compiler is remotely sane. In C++, including this in two C++ translation units that set the NDEBUG flag differently creates an ODR violation. The C++ solution to this problem was a system where each translation unit enforces its own pre- and post- conditions (potentially 4x evaluations), and contracts act as carefully crafted exceptions to the vast number of complicated rules added on top. An example is how observable behavior is a workaround for C++ refusing to adopt C's fix for time-traveling UB. Lisa Lippincott did a great talk on this last year: https://youtu.be/yhhSW-FSWkE https://youtu.be/yhhSW-FSWkE There's not much left of Contracts once you strip away the stuff that doesn't make sense in C. I don't think you'd miss anything by simply adding hygenic macros to assert.h as the author here does, except for the 4x caller/callee verification overhead that they enforce manually. I don't think that should be enforced in the standard though. I find hidden, multiple evaluation wildly unintuitive, especially if some silly programmer accidentally writes an effectful condition.
- 1718627440 1y ago
  I think the main point of pre- and post-conditions is, that the compiler can see them and prove that they match and will never be triggered. There probably will be a compiler flag for outputting all non-proved pre/postconditions, there is already -fanalyzer. I think these conditions should be part of the type signature, different to what was suggested in the otherwise good talk you cited.
  - zozbot234 1y ago
    > the compiler can see them and prove that they match and will never be triggered This is a huge challenge for a C-like language with pervasive global state. Might be more feasible for something like Rust, but still very difficult.
    - 1y ago
kstenerud 1y ago
I'm not sure I'm understanding this correctly... Given the examples, the author wants to ensure that 0 is not a possible input value, and NULL is not a possible output value. This could be achieved with a simple inline wrapper function that checks pre and post conditions and does abort() accordingly, without all of this extra ceremony But regardless of the mechansim you're left with another far more serious problem: You've now introduced `panic` to C. And panics are bad. Panics are landmines just waiting for some unfortunate circumstance to crash your app unexpectedly, which you can't control because control over error handling has now been wrested from you. It's why unwrap() in Rust is a terrible idea. It's why golang's bifurcated error mechanisms are a mess (and why, surprise surprise, the recommendation is to never use panic).
- integricho 1y ago
  Though is there a significant difference in which is more bad between running into undefined behavior and panic?
  - ost-ing 1y ago
    Exactly, panicking is a safer way to handle the situation rather than memory access violations
    - AlotOfReading 1y ago
      Safer in what sense? We have no idea whether this hypothetical code is in a userspace application that can exit safely at any time or a hard real time system where panicking could destroy hardware. A lot of important programs (like the Linux kernel) don't operate strictly on the exact letter of the standard's UB semantics. They do things like add compiler flags to specify certain behaviors, or assume implementation details.
      - imtringued 1y ago
        I will never understand how C developers can catastrophize over Rust panics, a language that has a panicless "_try" version of every panic causing function that returns a Result instead, while simultaneously accepting the infinite growth of ever harder to avoid UB in C/C++ and telling people to never have undefined behavior in their code. If you think dealing with undefined behavior is easy and you assume that people have verified that their software triggers no undefined behavior at runtime is fair game, then you should grant that assumption in favor of Rust developers having done the same with their panics, because avoiding panics is child's play in comparison to avoiding UB. I don't know what it is about panics that triggers some mania in people. UB does not interrupt the program and therefore allows memory corrupt and complete takeover of a program and the entire system as a consequence. C developers are like "this is fine", while sitting in a house that is burning down. There used to be a pretty blatant hibernation bug with AMD GPUs on Linux that essentially crashes your desktop session upon turning your computer on from hibernation. I've also had a wifi driver segfault on login that forcibly logged you out so you couldn't login like 9 years ago. C doesn't magically fix these problems by not having an explicit concept of panics. You still need to write software that is correct and doesn't crash before you push an update. There is no meaningful difference between a correctness bug and a panic triggering condition with the exception that the panic forces you to acknowledge the error during development, meaning it is more likely that the correctness bug gets caught in the first place.
unit149 1y ago
[dead]
sirwhinesalot 1y ago
Contracts getting proposed but still no slice/span type or even standardization of that new clang feature that makes f(int n, int a[n]) Actually do what it looks like it does. Sigh
- veltas 1y ago
  You can do f(int n, int (*a)[n]) and it does what it looks like, since C99. https://godbolt.org/z/8dfKMrGqv https://godbolt.org/z/8dfKMrGqv
  - sirwhinesalot 1y ago
    That's an entirely different thing (VLAs)
    - veltas 1y ago
      There's no VLA in my example.
      - sirwhinesalot 1y ago
        Your example doesn't do any bounds checks, it just lets you get the sizeof. And the reason the sizeof works is the VLA infrastructure (which is not supported by MSVC so it won't compile the code). What I want is -fbounds-safety from clang.
        navi-desu 1y ago
        it does do bounds checks if you -fsanitize=bounds, in gcc at least (and msvc is stuck on partial c11 support to this day, so imo, i don't quite think it's a fair target when comparing things to new features anyway)
- miropalmu 1y ago
  What do you mean no slice/span type? https://en.cppreference.com/w/cpp/container/span.html https://en.cppreference.com/w/cpp/container/span.html Or if you want multidimensional span: https://en.cppreference.com/w/cpp/container/mdspan.html https://en.cppreference.com/w/cpp/container/mdspan.html
1718627440 1y ago
The author writes that contract_assume invokes undefined behaviour when the assertion fails: #define contract_assume(COND, ...) do { if (!(COND)) unreachable(); } while (false) But this means that the compiler is allowed to e.g. reorder the condition check and never output the message. (Or invoke nasal demons, of course). This doesn't make much sense. I get that you want the compiler to maybe do nothing different or panic after the assertion failed, but only really after triggering the assertion and the notion of after doesn't really exist with undefined behaviour. The whole program is simply invalid.
- babaceca 1y ago
  There's no assertion required by spec. To the brain of a compiler writer UB means "the standard doesn't specify what should happen, therefore I can optimize with the assumption UB never happen." I disagree that this is how UB should be interpreted, but this fight is long lost. With that interpretation of UB, all `unreachable()` means is that the compiler is allowed to optimize as if this point in the code will never be reached. The unreachable macro is standard in C23 but all major compilers provide a way to do it, for all versions of the language. So if you have a statement like `if (x > 3) unreachable()` that serves as both documentation of the accepted values, as a constraint that the optimizer can understand - if x is an unsigned int, it will optimize with the assumption that the only possible values are 0,1,2. Of course in a debug build a sane compiler would have `unreachable()` trigger an assert fail, but they're not required to, and in release they most definitely won't do so, so you can't rely on it as a runtime check.
  - 1718627440 1y ago
    > so you can't rely on it as a runtime check. Exactly. But we already have unreachable and assert. The whole point of contracts is, that they are checked by the compiler (when the compiler invoker asks for it). Having the contract invoke UB in the fail case means that instead of replacing the error return with a diagnostic provable by the compiler, you replace the error return with potential corruption. In which case is that ever the right choice?
tempodox 1y ago
> Here unreacheable() is the new macro from C23 (and C++23) that makes the behaviour undefined whenever the branch of the invocation is reached. I cannot, in good conscience, use a technology that adds even more undefined behavior. Instead it reinforces my drive to avoid C whenever I can and use OCaml or Rust instead.
- 1718627440 1y ago
  I think it is good to explicitly invoke UB. It makes it much more obvious in the code, where it is intended and where not. It's a way to specify that this point in code is never reached, the code can't deal with it and I don't even care what the compiler does in this case. It's also a good thing to tell the compiler that the programmer intends that this case will never happen, so that the static analyzer can point out ways through the code, where it actually does.
- aw1621107 1y ago
  For what it's worth, Rust has std::hint::unreachable_unchecked() which does exactly the same thing.
tpoacher 1y ago
One of the biggest problems I find with contracts whenever contracts are mentioned is that nobody seems to have a really clear definition of what exactly a contract 'is' or 'should be' (with the exception of languages where contracts are a formal part of the language, that is). I find the general concept incredibly useful, and apply it in the more general sense to my own code, but there's always a bit of "what do I actually want contracts to mean / do here" back-and-forth before they're useful. PS: I do like how D does contracts; though I admit I haven't used D much yet, to my great regret, so I can't offer my experience of how well contracts actually work in D.
- bmn__ 1y ago
  No wonder it looks less than awesome to you. A contract is just a hack. Ideally, it should not exist because the type system already covers the programmer's intent. Languages that have shitty types which cannot express very much must work around the problem with contracts.
  - 1718627440 1y ago
    Aren't contracts a feature of the type system? They encode a specific type that differs from the base type by a more complex predicate, like a constraint check in SQL.
  - tpoacher 1y ago
    Partially agree, but only for a very narrow definition of what is a contract, which again is the problem stated above. A good contract system may in fact rely on type-safety as part of its implementation, but types do not necessarily cover all aspects of contracts (unless you're referring to the full gamut of theoretical generalisations of things like dependent types, substructural types, constraint logic programming, etc), and are also not necessarily limited to things that only apply at compile-time.
guerrilla 1y ago
I don't know what C++ is trying to do, but does everyone know about frama-c[1]? 1. https://frama-c.com/ https://frama-c.com/
deleted 1y ago
[deleted]

Contracts for C

108 points by joexbayer 1y ago

__d 1y ago

I like Eiffel. But if I want to use Eiffel, I’ll use Eiffel (or Sather). I’d rather C remained C. Maybe that’s just me?

jimbob45 1y ago
Java 24 and C# 9 resemble little of their first versions. C++ might as well not even be the same language at this point. Why are we so conservative with C but then so happily liberal with every other language?
- dmitrygr 1y ago
  Because there must be at least one refuge for the sane
- HexDecOctBin 1y ago
  People chose C because they liked C. Of course they don't want C to change. The only thing the ISO committee should be adding is stuff for filling in the holes in language (C23's Improved Tag Compatibility and __VA_OPT__ are good examples), not add features that were never part of C and were never supposed to be there. Your question can be reflected back to you: if you want an ever changing languages, go to Java, C# or C++, why mess with C?
  - xboxnolifes 1y ago
    > People chose C because they liked C. Of course they don't want C to change. The same thing can be said for every other language, yet they change.
    - oguz-ismail 1y ago
      Well they shouldn't have. It was much more fun to program in Python 2.7 and Java 7, I wouldn't touch those languages with a five feet pole these days
      - lifthrasiir 1y ago
        Why specifically Python 2.7 and not, like, 1.5? Python 1 and 2 are as different as 2 and 3 (that is, surprisingly not much).
    - WalterBright 1y ago
      A common thing people write about D is don't add any more features except for their feature proposals. :-)
  - brabel 1y ago
    This is funny because Java people say the same about Kotlin and Scala.
  - pjmlp 1y ago
    No, many people chose C, because they had to.
    - sarchertech 1y ago
      Yeah but those people are running it on some platform where it’s the only choice. And they are probably running a subset of C99. The likelihood of new features ever making it to those platforms is close to zero.
      - pjmlp 1y ago
        There is hardly any new C compiler that isn't C11.
        sarchertech 1y ago
        I’ve been out of embedded for a bit but last I checked almost nothing actually implemented all of C11?
        pjmlp 1y ago
        There is hardly any compiler worth using that isn't a fork of either GCC or clang. So unless they are stuck on a pre-historic fork, they support C11 as much as clang and GCC do. Exception for stuff like PIC, Z80,... Which didn't even support proper C on their glory days.
  - WalterBright 1y ago
    C added the absurd normalized Unicode identifiers.
- nananana9 1y ago
  The complexity of C# and C++ should be a warning, not something to strive towards. C++ has 3 reasonable implementations, C has hundreds, for all sorts of platforms, where you don't get anything else. Most C developers don't want a modern C, they want a reliable C. WG14 should be pushing for clarifications on UB, the memory and threading model, documenting where implementations differ, and what parts of the language can be relied and what not. Nobody really needs a new way to do asserts, case ranges, or a new way to write the word "NULL".
  - lifthrasiir 1y ago
    C++ historically had much more implementations. It is probably more about the availability of quality compilers that are free to use and adapt, because even in C most new compilers for niche platforms are now based on GCC or clang for the practical reason.
    - pjmlp 1y ago
      Both implementated in C++. As someone that remembers the t-shirts with "my compiler compiles yours" that some C folks used to wear, it is kind of ironic having that turned around on them.
  - motorest 1y ago
    > The complexity of C# and C++ should be a warning, not something to strive towards. I think this talk about "complexity" is a red herring. C++ remains one of the most popular languages ever designed, and one of the key reasons is that since C++11 the standardization effort picked up steam and started including features that the developer community wanted and was eager to get. I still recall the time that randos criticized C++ for being a dead language and being too minimalistic and spartan. > C++ has 3 reasonable implementations, C has hundreds, for all sorts of platforms, where you don't get anything else. I don't understand what point you are trying to make. Go through the list of the most popular programming languages, and perhaps half of them are languages which only have a single implementation. What compelled you to criticize C++ for having at least 3 production-quality implementations? > Most C developers don't want a modern C, they want a reliable C. You speak only for yourself. Your personal opinion is based on survivorship bias. I can tel you that as a matter of fact a key reason why the likes of Rust took off was that people working with low-level systems programming were desperate for a C with better developer experience and sane and usable standard library. > Nobody really needs a new way to do asserts, case ranges, or a new way to write the word "NULL". Again, you speak for yourself, and yourself alone. You believe you don't need new features. That's fine. But you speak for yourself.
OCTAGRAM 1y ago
Eiffel has unsolicited tracing garbage collection. For TGC-free programming there is Ada
veltas 1y ago
Truly I agree, but if we can add features to improve C codebases without rewriting them then that's a win, and you can just ignore them if you don't like them (as I will), but to the people where this has benefit they can be used.
pjmlp 1y ago
Languages are software products like everything else in computing, either they evolve or they whither and die. C especially was designed with lots of security defects, and had it not been for UNIX being available for free, it would probably never taken off.
- HexDecOctBin 1y ago
  More likely they evolve AND they whither and die. The number of software I have stopped using due to bad updates is much higher than those with not enough updates.
johnisgood 1y ago
Ada / SPARK has contracts, too, that can be proven at compile-time. In fact, Ada alone suffices, it has pre- and post-conditions. I think Ada has more libraries than Eiffel does. Does anyone even write Eiffel? I am really curious if it is still alive anywhere, in some form.
- WalterBright 1y ago
  Eiffel failed largely because of licensing restrictions.
flykespice 1y ago
Are you being really honest with yourself that you would renounce c90, c99 additions to stay with the original language as it was introduced in K&R C book?

WalterBright 1y ago

Digital Mars C++ has had contracts since, oh, the early 1990s? https://www.digitalmars.com/ctg/contract.html https://www.digitalmars.com/ctg/contract.html

motorest 1y ago
> Digital Mars C++ has had contracts since, oh, the early 1990s? I think that implementations trying out their own experimental features is normal and expected. Ideally, standards would be pull-based instead of push-based. The real question is what prevented this feature from being proposed to the standardization committee.
- arunc 1y ago
  It was proposed by Walter and denied by Stroustroup, probably to save C++. Karma hits back and he is trying to save C++ from Rust.
  - pjmlp 1y ago
    People keep forgetting C++ design is driven by 300+ people, and the features that get into the language go to elections, that they have to win. Stroustoup has one vote, not everything he advocates for wins votes, including having a saner C++ (Remember the Vasa paper).
  - motorest 1y ago
    > It was proposed by Walter and denied by Stroustroup, probably to save C++. Citation needed. For starters, where is the paper?
    - shakna 1y ago
      Well, there's this list Stroustrup offers, of systems in C++ that he would reject: [0] [0] https://open-std.org/JTC1/SC22/WG21/docs/papers/2018/p0977r0.pdf https://open-std.org/JTC1/SC22/WG21/docs/papers/2018/p0977r0...

taminka 1y ago

do i understand correctly that there's nothing preventing someone from adding a postcondition check X and then just not implementing it inside the function? wouldn't this just mean that now the ub is triggered by the post()'s `unceachable()` instead of whatever ub would happen w/, say, dereferencing a null pointer, as a consequence of not actually implementing post check X? so it's just for speed optimisations then? from reading about contracts for C before i assumed it would be like what cake[1] does, which actually compile time enforces pointer (non)nullability, as well as resource ownership and a bunch of other stuff, very cool project, check it out if you haven't seen it yet :) [1]https://github.com/thradams/cake https://github.com/thradams/cake

AlotOfReading 1y ago

There's a bit of an impedence mismatch with Contracts in C because C++ contracts exist partially to rectify the fact that <cassert> is broken in C++. Let's say you have a header lib.h: inline int foo(int i) { assert(i > 0); //... } In C, this function is unspecified behavior that will probably work if the compiler is remotely sane. In C++, including this in two C++ translation units that set the NDEBUG flag differently creates an ODR violation. The C++ solution to this problem was a system where each translation unit enforces its own pre- and post- conditions (potentially 4x evaluations), and contracts act as carefully crafted exceptions to the vast number of complicated rules added on top. An example is how observable behavior is a workaround for C++ refusing to adopt C's fix for time-traveling UB. Lisa Lippincott did a great talk on this last year: https://youtu.be/yhhSW-FSWkE https://youtu.be/yhhSW-FSWkE There's not much left of Contracts once you strip away the stuff that doesn't make sense in C. I don't think you'd miss anything by simply adding hygenic macros to assert.h as the author here does, except for the 4x caller/callee verification overhead that they enforce manually. I don't think that should be enforced in the standard though. I find hidden, multiple evaluation wildly unintuitive, especially if some silly programmer accidentally writes an effectful condition.

1718627440 1y ago
I think the main point of pre- and post-conditions is, that the compiler can see them and prove that they match and will never be triggered. There probably will be a compiler flag for outputting all non-proved pre/postconditions, there is already -fanalyzer. I think these conditions should be part of the type signature, different to what was suggested in the otherwise good talk you cited.
- zozbot234 1y ago
  > the compiler can see them and prove that they match and will never be triggered This is a huge challenge for a C-like language with pervasive global state. Might be more feasible for something like Rust, but still very difficult.
  - 1y ago

kstenerud 1y ago

I'm not sure I'm understanding this correctly... Given the examples, the author wants to ensure that 0 is not a possible input value, and NULL is not a possible output value. This could be achieved with a simple inline wrapper function that checks pre and post conditions and does abort() accordingly, without all of this extra ceremony But regardless of the mechansim you're left with another far more serious problem: You've now introduced `panic` to C. And panics are bad. Panics are landmines just waiting for some unfortunate circumstance to crash your app unexpectedly, which you can't control because control over error handling has now been wrested from you. It's why unwrap() in Rust is a terrible idea. It's why golang's bifurcated error mechanisms are a mess (and why, surprise surprise, the recommendation is to never use panic).

integricho 1y ago
Though is there a significant difference in which is more bad between running into undefined behavior and panic?
- ost-ing 1y ago
  Exactly, panicking is a safer way to handle the situation rather than memory access violations
  - AlotOfReading 1y ago
    Safer in what sense? We have no idea whether this hypothetical code is in a userspace application that can exit safely at any time or a hard real time system where panicking could destroy hardware. A lot of important programs (like the Linux kernel) don't operate strictly on the exact letter of the standard's UB semantics. They do things like add compiler flags to specify certain behaviors, or assume implementation details.
    - imtringued 1y ago
      I will never understand how C developers can catastrophize over Rust panics, a language that has a panicless "_try" version of every panic causing function that returns a Result instead, while simultaneously accepting the infinite growth of ever harder to avoid UB in C/C++ and telling people to never have undefined behavior in their code. If you think dealing with undefined behavior is easy and you assume that people have verified that their software triggers no undefined behavior at runtime is fair game, then you should grant that assumption in favor of Rust developers having done the same with their panics, because avoiding panics is child's play in comparison to avoiding UB. I don't know what it is about panics that triggers some mania in people. UB does not interrupt the program and therefore allows memory corrupt and complete takeover of a program and the entire system as a consequence. C developers are like "this is fine", while sitting in a house that is burning down. There used to be a pretty blatant hibernation bug with AMD GPUs on Linux that essentially crashes your desktop session upon turning your computer on from hibernation. I've also had a wifi driver segfault on login that forcibly logged you out so you couldn't login like 9 years ago. C doesn't magically fix these problems by not having an explicit concept of panics. You still need to write software that is correct and doesn't crash before you push an update. There is no meaningful difference between a correctness bug and a panic triggering condition with the exception that the panic forces you to acknowledge the error during development, meaning it is more likely that the correctness bug gets caught in the first place.

unit149 1y ago

[dead]

sirwhinesalot 1y ago

Contracts getting proposed but still no slice/span type or even standardization of that new clang feature that makes f(int n, int a[n]) Actually do what it looks like it does. Sigh

veltas 1y ago
You can do f(int n, int (*a)[n]) and it does what it looks like, since C99. https://godbolt.org/z/8dfKMrGqv https://godbolt.org/z/8dfKMrGqv
- sirwhinesalot 1y ago
  That's an entirely different thing (VLAs)
  - veltas 1y ago
    There's no VLA in my example.
    - sirwhinesalot 1y ago
      Your example doesn't do any bounds checks, it just lets you get the sizeof. And the reason the sizeof works is the VLA infrastructure (which is not supported by MSVC so it won't compile the code). What I want is -fbounds-safety from clang.
      - navi-desu 1y ago
        it does do bounds checks if you -fsanitize=bounds, in gcc at least (and msvc is stuck on partial c11 support to this day, so imo, i don't quite think it's a fair target when comparing things to new features anyway)
miropalmu 1y ago
What do you mean no slice/span type? https://en.cppreference.com/w/cpp/container/span.html https://en.cppreference.com/w/cpp/container/span.html Or if you want multidimensional span: https://en.cppreference.com/w/cpp/container/mdspan.html https://en.cppreference.com/w/cpp/container/mdspan.html

1718627440 1y ago

The author writes that contract_assume invokes undefined behaviour when the assertion fails: #define contract_assume(COND, ...) do { if (!(COND)) unreachable(); } while (false) But this means that the compiler is allowed to e.g. reorder the condition check and never output the message. (Or invoke nasal demons, of course). This doesn't make much sense. I get that you want the compiler to maybe do nothing different or panic after the assertion failed, but only really after triggering the assertion and the notion of after doesn't really exist with undefined behaviour. The whole program is simply invalid.

babaceca 1y ago
There's no assertion required by spec. To the brain of a compiler writer UB means "the standard doesn't specify what should happen, therefore I can optimize with the assumption UB never happen." I disagree that this is how UB should be interpreted, but this fight is long lost. With that interpretation of UB, all `unreachable()` means is that the compiler is allowed to optimize as if this point in the code will never be reached. The unreachable macro is standard in C23 but all major compilers provide a way to do it, for all versions of the language. So if you have a statement like `if (x > 3) unreachable()` that serves as both documentation of the accepted values, as a constraint that the optimizer can understand - if x is an unsigned int, it will optimize with the assumption that the only possible values are 0,1,2. Of course in a debug build a sane compiler would have `unreachable()` trigger an assert fail, but they're not required to, and in release they most definitely won't do so, so you can't rely on it as a runtime check.
- 1718627440 1y ago
  > so you can't rely on it as a runtime check. Exactly. But we already have unreachable and assert. The whole point of contracts is, that they are checked by the compiler (when the compiler invoker asks for it). Having the contract invoke UB in the fail case means that instead of replacing the error return with a diagnostic provable by the compiler, you replace the error return with potential corruption. In which case is that ever the right choice?

tempodox 1y ago

> Here unreacheable() is the new macro from C23 (and C++23) that makes the behaviour undefined whenever the branch of the invocation is reached. I cannot, in good conscience, use a technology that adds even more undefined behavior. Instead it reinforces my drive to avoid C whenever I can and use OCaml or Rust instead.

1718627440 1y ago
I think it is good to explicitly invoke UB. It makes it much more obvious in the code, where it is intended and where not. It's a way to specify that this point in code is never reached, the code can't deal with it and I don't even care what the compiler does in this case. It's also a good thing to tell the compiler that the programmer intends that this case will never happen, so that the static analyzer can point out ways through the code, where it actually does.
aw1621107 1y ago
For what it's worth, Rust has std::hint::unreachable_unchecked() which does exactly the same thing.

tpoacher 1y ago

One of the biggest problems I find with contracts whenever contracts are mentioned is that nobody seems to have a really clear definition of what exactly a contract 'is' or 'should be' (with the exception of languages where contracts are a formal part of the language, that is). I find the general concept incredibly useful, and apply it in the more general sense to my own code, but there's always a bit of "what do I actually want contracts to mean / do here" back-and-forth before they're useful. PS: I do like how D does contracts; though I admit I haven't used D much yet, to my great regret, so I can't offer my experience of how well contracts actually work in D.

bmn__ 1y ago
No wonder it looks less than awesome to you. A contract is just a hack. Ideally, it should not exist because the type system already covers the programmer's intent. Languages that have shitty types which cannot express very much must work around the problem with contracts.
- 1718627440 1y ago
  Aren't contracts a feature of the type system? They encode a specific type that differs from the base type by a more complex predicate, like a constraint check in SQL.
- tpoacher 1y ago
  Partially agree, but only for a very narrow definition of what is a contract, which again is the problem stated above. A good contract system may in fact rely on type-safety as part of its implementation, but types do not necessarily cover all aspects of contracts (unless you're referring to the full gamut of theoretical generalisations of things like dependent types, substructural types, constraint logic programming, etc), and are also not necessarily limited to things that only apply at compile-time.

guerrilla 1y ago

I don't know what C++ is trying to do, but does everyone know about frama-c[1]? 1. https://frama-c.com/ https://frama-c.com/

deleted 1y ago

[deleted]