6 ms·

IMHO preconditions and postconditions are a big win for Ada. I missed them in Rust, so wrote the Rust "assertables" crate, which provides runtime assert express

by jph 3y ago

IMHO preconditions and postconditions are a big win for Ada. I missed them in Rust, so wrote the Rust "assertables" crate, which provides runtime assert expressions for a bunch of typical cases such as comparing numbers, strings, lists, IO, etc. Rust code to assert a runtime precondition or postcondition a > b then handle it as you wish: assert_gt_as_result!(a, b) -> Result https://crates.io/crates/assertables https://crates.io/crates/assertables

mmoskal 3y ago
There is also anyhow::ensure!() (which is more of a requires() but anyhow...)
saagarjha 3y ago
Why the specialized API, rather than (say) precondition(foo == bar)?
- masklinn 3y ago
  Probably to get better error messages, same as assert_eq, otherwise you need a procedural macro to take appart the entire expression which is way more complicated and more expensive.
- jph 3y ago
  Merely because the "assert" wording is more familiar to more Rust developers because it's similar to typical test code, and can create better error messages with details. For what you're asking, the assertables crate has a macro that will handle any condition: assert_as_result!(condition) -> Result And you can alias it as you wish such as: use assertables::assert_as_result as precondition; And now you can write what you're suggesting: precondition(a == b)
GuB-42 3y ago
I wish more languages supported that natively, starting with C and C++. The most typical example, in C, output arguments, passed by pointer, a pattern that I also use in C++ because I find passing by non-const reference error-prone since it is not obvious looking at the calling code that an argument may be modified. But what about NULL? Sometimes it is a good thing that NULL is allowed, sometimes, it doesn't make sense. So again, not obvious. So what to we do? You can document it of course, but the problem is that compilers don't read the docs, and therefore can't tell you if you are doing it wrong. You can play it safe, and design your API so that NULL is always an option, and avoid NULL when using others APIs, but it leads to unnecessary and performance-impacting checks. Preconditions and postconditions would solve that problem: if you pass an argument that can be NULL to a function that doesn't accept NULL, the compiler can warn you. Plus, there is optimization potential, in the same way that C/C++ does with undefined behavior, but this is explicit. You also can also get the choice between safe (runtime checks) or fast (undefined behavior) at compile time. Making it a core feature of the language rather than an extension (like your rust crate) will help compilers and other tools to take full advantage of what it brings.
- Arnavion 3y ago
  Microsoft's compiler has that ability with SAL annotations. But yes a standard way to do it would be nice. https://learn.microsoft.com/en-us/cpp/code-quality/using-sal-annotations-to-reduce-c-cpp-code-defects https://learn.microsoft.com/en-us/cpp/code-quality/using-sal...
- throw0101b 3y ago
  * https://en.wikipedia.org/wiki/Assert.h https://en.wikipedia.org/wiki/Assert.h ? C11 and C++11 also have compile-time static variants.
- summerlight 3y ago
  https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2900r1.pdf https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p29... C++ is preparing this for years, though it's uncertain when it will actually land in C++.
- mhh__ 3y ago
  D has contract programming e.g. `in(param < 0)` before { I don't think there's all that much that a typical compiler will do with them however sophisticated enough type system I can see some wins.
- nurettin 3y ago
  > I find passing by non-const reference error-prone since it is not obvious looking at the calling code that an argument may be modified. VS code makes it pretty obvious by adding a visual & prefix to the argument. I hope that kind of visual help becomes widely adopted.
- 8n4vidtmkvmk 3y ago
  I've started using abseil null/no null https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://github.com/abseil/abseil-cpp/blob/master/absl/base/nullability.h&ved=2ahUKEwjrrYbq7fGCAxWOLUQIHe4XBhMQFnoECBAQAQ&usg=AOvVaw2pa6BSJIUtJs0Mld7Zj2-I https://www.google.com/url?sa=t&source=web&rct=j&opi=8997844... We have a linter that will try to catch cases where you didn't null check but the field is nullable
skyde 3y ago
C# used to have postconditions and verify them at compile time. But this has been deprecated :( I wish I knew why they removed it. https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts https://learn.microsoft.com/en-us/dotnet/framework/debug-tra...
- pjmlp 3y ago
  It was only available on enterprise versions, and most likely Microsoft has concluded not enough people were paying for it, nor they wanted to keep it for free, porting them into modern .NET runtime.
nextaccountic 3y ago
Rust has this https://crates.io/crates/contracts https://crates.io/crates/contracts
- nextaccountic 3y ago
  And I can't edit but, Rust can statically check contracts too https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_than_rust/k7m7tl5/ https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_...
- kaba0 3y ago
  Isn’t it its own language to a degree? Which may or may not be a bad thing in itself, but I do think there is value in having it natively available.
  - nextaccountic 3y ago
    It is, but that's just Rust's style. The stdlib is deliberately kept small, so that an ecosystem would flourish. In the design by contract case, there's a lot of experimentation (I linked this https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_than_rust/k7m7tl5/ https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_... in another comment) and while all of them are converging to the same syntax, they all have wildly different implementations. Perhaps the stdlib could provide a base syntax for contracts, with extensibility APIs so that libraries or compiler plugins or external tooling can determine whether the contract is checked at runtime or at compile time, and by which method. But that demands a lot of design, because once something is in the stdlib and stabilized, it's here forever.
mostlylurks 3y ago
Preconditions and postconditions seem like the wrong way to go about solving the issue they try to solve. They are essentially a secondary type system that tries to express information not expressed by the primary type system in a way that is awkwardly disconnected from the primary type system. You could instead just implement the functionality needed to incorporate that information into the primary type system. In practice this would result in an implementation of dependent types, which is fine.
- kaba0 3y ago
  > implementation of dependent types, which is fine. Which you have to prove, which is absolutely non-trivial. I guess it could be made into a runtime check as well where static analysis is not possible, but that seems to be a quite hard to reason about language regarding performance.
  - mycall 3y ago
    .NET Code Contracts has both compile time and runtime checks, although it always felt like a bolted on solution even though it is baked into the framework. I guess this is why it didn't carry forward into the .NET Core rewrite.
- HacklesRaised 3y ago
  Betrand Meyer is coming for you... ;-) He's not, he would respect your opinion, but design by contract was on of the key foundations of Eiffel, and I have a soft spot for Eiffel.
- throwawaymaths 3y ago
  Maybe you don't have to encode everything in the type system? Also: Maybe not everything goes in the compiler?
adrianmonk 3y ago
It seems like there's a very minor error under the "Why use this?" section: assert_gt!(value1, value2); // value1 ≥ value2 That should be ">" rather than "≥". (Or "assert_ge" rather than "assert_gt".)
- jph 3y ago
  You're right. Thank you! Fixing it now.

by jph 3y ago

mmoskal 3y ago

There is also anyhow::ensure!() (which is more of a requires() but anyhow...)

saagarjha 3y ago

Why the specialized API, rather than (say) precondition(foo == bar)?

masklinn 3y ago
Probably to get better error messages, same as assert_eq, otherwise you need a procedural macro to take appart the entire expression which is way more complicated and more expensive.
jph 3y ago
Merely because the "assert" wording is more familiar to more Rust developers because it's similar to typical test code, and can create better error messages with details. For what you're asking, the assertables crate has a macro that will handle any condition: assert_as_result!(condition) -> Result And you can alias it as you wish such as: use assertables::assert_as_result as precondition; And now you can write what you're suggesting: precondition(a == b)

GuB-42 3y ago

I wish more languages supported that natively, starting with C and C++. The most typical example, in C, output arguments, passed by pointer, a pattern that I also use in C++ because I find passing by non-const reference error-prone since it is not obvious looking at the calling code that an argument may be modified. But what about NULL? Sometimes it is a good thing that NULL is allowed, sometimes, it doesn't make sense. So again, not obvious. So what to we do? You can document it of course, but the problem is that compilers don't read the docs, and therefore can't tell you if you are doing it wrong. You can play it safe, and design your API so that NULL is always an option, and avoid NULL when using others APIs, but it leads to unnecessary and performance-impacting checks. Preconditions and postconditions would solve that problem: if you pass an argument that can be NULL to a function that doesn't accept NULL, the compiler can warn you. Plus, there is optimization potential, in the same way that C/C++ does with undefined behavior, but this is explicit. You also can also get the choice between safe (runtime checks) or fast (undefined behavior) at compile time. Making it a core feature of the language rather than an extension (like your rust crate) will help compilers and other tools to take full advantage of what it brings.

Arnavion 3y ago
Microsoft's compiler has that ability with SAL annotations. But yes a standard way to do it would be nice. https://learn.microsoft.com/en-us/cpp/code-quality/using-sal-annotations-to-reduce-c-cpp-code-defects https://learn.microsoft.com/en-us/cpp/code-quality/using-sal...
throw0101b 3y ago
* https://en.wikipedia.org/wiki/Assert.h https://en.wikipedia.org/wiki/Assert.h ? C11 and C++11 also have compile-time static variants.
summerlight 3y ago
https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2900r1.pdf https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p29... C++ is preparing this for years, though it's uncertain when it will actually land in C++.
mhh__ 3y ago
D has contract programming e.g. `in(param < 0)` before { I don't think there's all that much that a typical compiler will do with them however sophisticated enough type system I can see some wins.
nurettin 3y ago
> I find passing by non-const reference error-prone since it is not obvious looking at the calling code that an argument may be modified. VS code makes it pretty obvious by adding a visual & prefix to the argument. I hope that kind of visual help becomes widely adopted.
8n4vidtmkvmk 3y ago
I've started using abseil null/no null https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://github.com/abseil/abseil-cpp/blob/master/absl/base/nullability.h&ved=2ahUKEwjrrYbq7fGCAxWOLUQIHe4XBhMQFnoECBAQAQ&usg=AOvVaw2pa6BSJIUtJs0Mld7Zj2-I https://www.google.com/url?sa=t&source=web&rct=j&opi=8997844... We have a linter that will try to catch cases where you didn't null check but the field is nullable

skyde 3y ago

C# used to have postconditions and verify them at compile time. But this has been deprecated :( I wish I knew why they removed it. https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts https://learn.microsoft.com/en-us/dotnet/framework/debug-tra...

pjmlp 3y ago
It was only available on enterprise versions, and most likely Microsoft has concluded not enough people were paying for it, nor they wanted to keep it for free, porting them into modern .NET runtime.

nextaccountic 3y ago

Rust has this https://crates.io/crates/contracts https://crates.io/crates/contracts

nextaccountic 3y ago
And I can't edit but, Rust can statically check contracts too https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_than_rust/k7m7tl5/ https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_...
kaba0 3y ago
Isn’t it its own language to a degree? Which may or may not be a bad thing in itself, but I do think there is value in having it natively available.
- nextaccountic 3y ago
  It is, but that's just Rust's style. The stdlib is deliberately kept small, so that an ecosystem would flourish. In the design by contract case, there's a lot of experimentation (I linked this https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_than_rust/k7m7tl5/ https://old.reddit.com/r/rust/comments/17miqiu/is_ada_safer_... in another comment) and while all of them are converging to the same syntax, they all have wildly different implementations. Perhaps the stdlib could provide a base syntax for contracts, with extensibility APIs so that libraries or compiler plugins or external tooling can determine whether the contract is checked at runtime or at compile time, and by which method. But that demands a lot of design, because once something is in the stdlib and stabilized, it's here forever.

mostlylurks 3y ago

Preconditions and postconditions seem like the wrong way to go about solving the issue they try to solve. They are essentially a secondary type system that tries to express information not expressed by the primary type system in a way that is awkwardly disconnected from the primary type system. You could instead just implement the functionality needed to incorporate that information into the primary type system. In practice this would result in an implementation of dependent types, which is fine.

kaba0 3y ago
> implementation of dependent types, which is fine. Which you have to prove, which is absolutely non-trivial. I guess it could be made into a runtime check as well where static analysis is not possible, but that seems to be a quite hard to reason about language regarding performance.
- mycall 3y ago
  .NET Code Contracts has both compile time and runtime checks, although it always felt like a bolted on solution even though it is baked into the framework. I guess this is why it didn't carry forward into the .NET Core rewrite.
HacklesRaised 3y ago
Betrand Meyer is coming for you... ;-) He's not, he would respect your opinion, but design by contract was on of the key foundations of Eiffel, and I have a soft spot for Eiffel.
throwawaymaths 3y ago
Maybe you don't have to encode everything in the type system? Also: Maybe not everything goes in the compiler?

adrianmonk 3y ago

It seems like there's a very minor error under the "Why use this?" section: assert_gt!(value1, value2); // value1 ≥ value2 That should be ">" rather than "≥". (Or "assert_ge" rather than "assert_gt".)

jph 3y ago
You're right. Thank you! Fixing it now.