Design By Contract

[KingOfThePirates]

As of right now, this discussion is expected to be super abstract.

Rust is a beautiful language because it is modern and built with common sense. Though it still lacks features that no modern language should. This discussion is only for one of those features. We are almost post-1.0, and, around that time, we should be thinking about how DBC, one of the most useful tools a programmer could use, should be used in Rust.

The only thing we have to worry about right now is when to actually have this discussion. It should be soon, but soon might mean many months from now.

• Should we wait for a certain feature to come out first? Which feature? Wait for more features, too?
• What else is needed or wanted to be done before we get into a DBC discussion?
• Should only conventions work it? What would they be? Should syntax for DBC exist?

So, when do you think official Rust-supported DBC solutions should be discussed?

[gsingh93]

I don't know much about this, but is this related: https://github.com/nrc/libhoare

Also, we're not post-1.0 yet :)

[KingOfThePirates]

The beta is not considered post-1.0?

[gsingh93]

Post 1.0 is after May 15th, when the real 1.0 is out.

[arielb1]

DBC looks like one of these things that should be a syntax extension.

[DiamondLovesYou]

@arielb1 I disagree. Syntax extensions have no access to type resolved results. I believe what one would actually want would be a compiler plugin.

[gsingh93]

@DiamondLovesYou I thought syntax extensions and compiler plugins were the same thing. Can you give an example of each?

[KingOfThePirates]

@gsingh93 I edited the tense in the original post.

@DiamondLovesYou I would also like an example of each.

[nrc]

@DiamondLovesYou what do you want type information for?

As it stands at the moment, there are many things which are compiler plugins - these include procedural macros (aka syntax extensions), pluggable lints, and pluggable llvm passes. We also expose an API to the compiler to allow building custom compilers which have access to type info and everything else the compiler does.

It seems to me that DBC can be (at least partially) implemented as a syntax extension (libhoare is a proof of concept of this). If there is lots of interest and use in a syntax extensions, then it might be worth experimenting with a custom compiler to support more DBC features which can't be implemented as a syntax extension. If that is successful, then I think we can discuss moving things into the compiler proper. As it stands I think any conversation about going straight to language features is not going to progress very far or quickly.

We should also have more powerful syntax extensions available in the medium term future, they should allow better syntax for things like DBC without having to have core language support.

[arielb1]

Anyway, what is design by contract? Rust has a powerful type system that already handles the 90% most popular propositions.

[arielb1]

I mean, the Rust type-system covers at least:

• parameter i can't be null (don't use an Option)
• parameter i and parameter j can't both be null (use an enum)
• parameter i must not be negative (use an unsigned type)
• parameter i may not be modified until so-and-so (use lifetimes)

And that's at least 80% of all propositions already.

[KingOfThePirates]

The purpose of Design By Contract is to make bugs almost non-exist at all times, thus very fast developing. The syntax for DBC is self-documenting, so you should almost never have a single comment in all your code, while at the same time, someone who has never taken even his or her first programming class can know exactly what your program does without any other documentation.

Design By Contract is a design concept for contractors to require that the world around them is in a certain state and for the world to be ensured by the contractor that the world will be in a specific state when the contractor's job is done. A contractor is a routine/method/procedure/function.

You can stop reading here, unless you want more info.

1. Caller of a routine calls the routine.
2. Require checks the routine's needs. If everything is as the caller was supposed to promise, move on. Else you get a compiler error that states which needs were not met.
3. The routine is now called
4. Ensure checks to make sure the routine did each and everything that it promised it would.
5. Goes back to the caller, like any other end of a called routine would.

An Eiffel example from The Pragmatic Programmer, page 114

sqrt: DOUBLE is
    -- Square root routine
require
    sqrt_arg_must_be_positive: Current >= 0;
--- ...
--- calculate square root here
--- ...
ensure
    ((Result*Result) - Current).abs <= epsilon*Current.abs;
  -- Result should be within error tolerance
end;

Though, this can be improved to be truly readable by fusing comments and what they are commenting into well-named routines. This, as a result, would eliminate repeating words, meaning your eyes should be able to glaze over just once and not waste time searching for something.

[gsingh93]

@KingOfThePirates Can you look at libhoare and see if that covers all the DBC constructs you need? If not, what's missing?

[KingOfThePirates]

I am sure it covers everything, except standards. I am not needing Rust to change anything at all.. for my personal projects. What I need, and of course everyone, is to have standards prepared for the future, when Rust is used by mainstream in businesses and such.

Plus Rust, being so early in development, why not have this powerful tool implemented in the language (I'd simply do it myself if I didn't start programming just since December)?

[gsingh93]

Plus Rust, being so early in development, why not have this powerful tool implemented in the language (I'd simply do it myself if I didn't start programming just since December)?

Because if we rush into things early, we're stuck with them forever. If this is a feature people want to use, they'll use the library, and if the library has enough use from the community, at that point it can be integrated into the language.

[KingOfThePirates]

I agree, which is part of the reason why I posted this. I wanted to know how many were interested. To me, who began programming with Code Complete, it seems silly to not implement these tools since we invented them. But I understand there are many who are unaware of concepts such as this one.

No matter what, there will be a language that is what I want, in the next decade or two, because if there isn't, I'll make it, but having it now would be awesome.

The reason why I am even using Rust as my first language while it is in early development is simply because I like it and its community. It isn't that bad that many of its members don't like every design concept that I like or as much as I like them. I still like this place so I'll stay here for awhile.

Since I'm new to programming, could you tell me why you think modern design concepts such as DBC are not simply in the standards of all coding?

[Diggsey]

@KingOfThePirates Techniques such as DBC have their place, but they are by no means universal (or even modern: DBC has been around since 1986!). With all of these sort of techniques, they're only useful if they can catch the kind of mistakes that you make often - in practice, I've found that DBC simply catches the wrong types of error, and that I'd have spent my time better writing more tests or documentation.
I'm sure for something like business logic, or data processing, contracts can be more useful, but that's kind of my point: it depends very much on the type of programming you are doing whether eg. DBC is worthwhile.

[KingOfThePirates]

@Diggsey Oh, thank you :)

[KingOfThePirates]

@nrc Thank you for your time and consideration.

Looks like we must listen to what nrc said on this matter.

• The current solution is libhoare.
• In order for the Rust gods to be motivated to create support for trickier DBC features, we need to experiment with a custom compiler to support these features, but before anyone bothers doing that, there are two recommended prerequisites:
  1. Lots of apparent interest.
  2. Lots of use in syntax extensions (procedural macros).
• We can look forward to "more powerful syntax extensions..in medium term future.." as well.

Rust gods: Please make sure to consider libhoare's wish list when making these "medium term future" syntax extension changes:

• work on methods as well as functions (requires changes to Rust compiler so that syntax extensions can be placed on methods as well as functions),
• object invariants (I think this would need compiler support, if it is possible at all. You would add [#invariant="..."] to a struct, enum, etc. and the invariant would be checked on entering and leaving every method defined in any impl for the object).

---

Edit 1 (Wednesday, April 22, 2015):

• Rust gods: Make sure syntax extensions can apply to constructs other than top level items.
• Useful info: "Although I did figure out how to register extension on impl methods. You need to use the MultiModifier variant, not the Modifier variant" (gsingh93, Allow syntax extensions to apply non-top level items #1069).
• Useful info: We can consider Rust-equivalent of tools such as KeY and OpenJML.

---

A higher up should close this if they deem it should be. I am unsure on whether or not others who might have Rust Design By Contract questions will be able to find this easily if it is closed.

P.S. This reddit post can branch off to some good information on DBC in Rust.

[Thiez]

It appears libhoare does not support loop invariants. Having those will be required (in almost all cases) to prove programs correct, so if we ever want to do static checking rather than runtime assertion checking those will be needed.

[gsingh93]

To add loop invariants, I'm assuming we'd want to annotate the loop with an attribute, and so syntax extensions would need to be extended to apply to constructs other than top level items

[gsingh93]

But honestly, static checking of things like this are better left to dependent type systems. I'd be fine just putting an assertion in my loop instead.

[Thiez]

I would assume that it is more likely that external tools will be written to perform static checking of Rust code than that the Rust type system will be extended in such a way that it is sufficiently powerful to perform full correctness proofs. Surely it would be awesome if we had the Rust-equivalent of tools such as KeY and OpenJML?

Edit: of course JML shows that the annotations do not need to be "real" annotations but can be inside comments, and it may be better if Rust goes that way as well. In that case no language support is required.

[UserAB1236872]

I think I'd prefer proofs to DBC. Though one could argue that DBC is a special, simple case of proofs, I think it would be impossible to implement a static proof system without accidentally implementing a DBC system as well.

Essentially, it would be nice to be able to have constructive proofs on types, evaluated at compile time. Note that these are constructive -- that is, not being able to create a proof makes no claims about its falsehood, but being able to make one does imply truth. Further, if an input doesn't meet certain guarantees, it should probably be a warning, because some things may not be statically provable (esp. due to the halting problem).

For instance, maybe I define a function that determines if a tree with the trait MyTree is finite, DFS will find the goal.

#[suggest]
proof<T> DFSComplete<T> for dfs<T> where T: MyTree {
    claim forall t: T, n: T::Node, is_finite(t) -> t.contains(n) -> (dfs(t,n).is_ok())

    // proof follows...
}

That is, for any tree implementing my trait, assuming that we have a proof that the function is_finite evaluates to true and a proof that t.contains(n) is true, running depth-first-search on my tree will return a path instead of None. (Assuming dfs returns Option<Vec<Node>> or something)

Certain proofs could also be suggested on inputs (#[suggest]), as opposed to required like in DBC. For instance, for some concrete implementations of MyTree, I may not be able to prove is_finite for various and somewhat obvious reasons, but I still want to use DFS on MyTree.

This would be a warning something like "Suggested proof DFSComplete cannot be validated because the assumption is_finite is not proven for MyConcreteTree. Use #[allow(no_proof)] to disable".

A stronger tag like #[require] could be used for DBC, where it's an outright error if a proof isn't provided, but I'd be worried about people trying to #[require] proofs too frequently on proofs that may not be provable for many valid inputs.

This would be extremely difficult to implement, though, and I wouldn't expect to see it for a long time, if ever. Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet. If this did exist, it may allow some compiler re-factoring, though, shuffing off a lot of the lifetime detection to the proof system.

[gsingh93]

I don't think baking this into the type system is a very good idea, as Rust would end up being a very different language. It seems like you're suggesting a dependent type system, and I don't think that's a good fit for Rust.

A better solution is probably to implement some front-end for existing tools that do formal verification, like krakatoa. The output can be sent to some other formal verification tool that can do the proving.

[rfielding]

I believe that APIs annotated with DBC enable the creation of extensively self-documenting code, and being able to specify - to the compiler - what compliant API usage means, no? If you have a collection of functions with pre/post conditions, you can generate state transition diagrams (where states are nodes specifying conditions, and edges are function calls that transition from precondition to postcondition nodes), and check/generate message sequence diagrams. It looks a lot like what you get out of LANGSEC where you have decidable protocols between modules (particularly at security sensitive points getting messages from sockets and disks.)

Even if only used as a library, not having DBC seems to be the key culprit in having large code bases that diverge from the documentation once implementation gets underway; as it's a matter of contracts making quite robust interfaces.

An important thing about contracts: You should not need to specify what the compiler can infer. And you should not to explicitly log or trace contract usage and contract violations. If a debug build logged contract-relevant messages and state changes, there would be little explicit logging being done at the boundaries between modules. I definitely agree that it gets close to having dependent types. But contract violations that are only detectable at run-time are a slightly different beast. In that case, it's more like having a transparent proxy around an allocated object to do something useful when the contract is violated (ie: panic or log the problem), which is different from error conditions that are part of the contract that must be observed by explicitly handling error conditions (ie: handling bad input as opposed to internal inconsistencies).

[nixpulvis]

It's too bad discussion has died down here, as this is a feature I'd kill to see in the language. Regardless of what compiler support it needs giving programmers a standard way of writing down contracts would be huge.

There has been a pretty wide variety of comments here about types. I'm not sure that Rust's contracts would need to change anything about the type system. Contracts are by design runtime checks that generally fit outside the type system of the language your in. You can even think to write weird contracts like one that ensures a function is only called after 6PM and before 8PM. There are a few subtitles with contracts in terms of implementation, but I think it's worth doing because it would allow programmers to fully express the invariants of their program to the level they desire, either as types (when possible) or as contracts for runtime checks. Rust appeals to a number of different people, for those who use it for C like speed, maybe contracts are a feature you will not use, but for those worried about safety in the most general sense of the word, contracts let you express more checks in a standard way.

Further contracts if implemented correctly are a huge help for debugging, as they can assign blame to the failing party. There have been a number of papers written on this, a good place to start might be http://www.ccs.neu.edu/racket/pubs/popl11-dfff.pdf.

[KingOfThePirates]

A thread doesn't die until all the subscribers do. This discussion will continue. I need to learn more to speak intelligently on the matter, though. I've been learning a new Industry for the past year. I'm finally at a point where I can get back to my passion at github :) But I think I started this conversation earlier than I was ready for. I don't know enough. But I will learn.

[KingOfThePirates]

@Jragonmiris Proofs look interesting. Might not solve the same problems Design By Contract solves, but it looks like it can be useful.

[burdges]

It's worth skimming the accepted RFC on impl specilization (closing, tracking). In that thread, idea that documentation practices of clearly stating invariance required of specializations could supersede parametricity proved influential.

It appears the proposed documentation practices would benefit substantially from a design by contract tool. In particular, we need an ability to specify that a method in a specialized impl operates the same as the default method in the impl it overloads, or at least operates mostly the same.

We envisioned humans checking these invariants, but perhaps one could reference the overloaded method to automate some checks. If this specification generates code, then it could only run in certain debugging situations, maybe quickcheck like tests, of course.

[Thiez]

A potential challenge is that Rust doesn't really have any notion of purity. Something like result > 1 can run arbitrary code, depending on the type of result and its PartialEq implementation, which can do arbitrarily impure things, e.g. perform IO, modify values in memory, etc. Of course sane implementations of PartialEq won't modify any visible state, when you want to prove something, you can't handwave these things.

If I may suggest a problem of a perhaps more limited scope: proving that unsafe blocks that do not involve FFI calls uphold the correct invariants. I think all the unsafe code in vec.rs is like this. Separation logic should probably be sufficient for this? I think when you can reason about memory and integers, you probably cover most such unsafe blocks.

[nixpulvis]

Might be best to focus on the runtime contract system, that alone is worth something since it's going to be more powerful than Rust's type system. Being able to check pre and post conditions with arbitrary rust code is the main feature I'd want. And maybe a nice syntax for creating and composing contracts.

Dealing with contracts with higher order functions is going to be the hairy part of the implementation most likely.

[gsingh93]

@socumbersome what would you provide that isn't already in https://github.com/nrc/libhoare?

[burdges]

It sounds like DBC is meant to operate below the type level? Even if so, an awful lot can be lifted to the type level with wrapper newtypes, so..

An idea might be built in debug assertion traits each with a single method that gets invoked at different places in debug builds:

• DebugAssertPassed - Checked whenever the type is passed to a function.
• DebugAssertReturned - Checked whenever the type is returned from a function.
• DebugAssertMutation - Checked a assignment to a mutable variable of this type occurs.
• DebugAssertSend - Checked whenever the type gets sent between threads, meaning whenever stored into types that require Send markers.
• DebugAssertDrop - Checked whenever the type is dropped, even if the type is Copy.

Aside from debug builds, there might be work on the LLVM side to make massively duplicated assertions optimize well, fast, correctly, etc.

As an aside, I think the units crate looks interesting for ensuring measurement unit-like invariants. There is probably more that could be done with more careful usage of wrapper types like that.

[socumbersome]

@Thiez - yes, being able to reason about purity looks important here. I wonder whether it would be best to first do #1631 and then DBC/PS, or just proceed with DBC/PS and, until Effect System is ready, check purity in some hacky way (if possible).

Also, a possibly crazy idea occurred to me -- maybe it would make sense to have impure computations inside preconditions as long as the following hold:

1. There is no IO in a "In" sense, that is getting input from the user
2. If running the precondition destroys some values (like arguments of the function), then they must implement Clone, so that they could be restored when executing body of function

Now, why on earth would I want IO in a "Out" sense (if I swapped the meaning by accident, I mean here reading from files etc.)? Well, for example, one could have a functions that performs some dangerous computations with chemicals or whatnot, and it's only safe to do that if some sensor has not too high temperature -- so, reading from a dynamically changing file! I don't know how far-fetched my example is, though :P
How do you think?

@gsingh93 - if we talk about DBC without PS and agree on separation of those, then in libhoare it's impossible to put invariants on objects (which is noted in a wish list). And that's something I certainly would want to see in fully-fledged DBC implementation.

[nixpulvis]

There is some precedence for stateful contracts, for example you could read the paper on Stateful Contracts for Affine Types which implements a runtime check similar to Rust's own type system in some ways.

Many of these limitations might be pragmatic, but not necessary for the design.

[JaneSmith]

I'd just like to chime in with my support for this. Coming from a C#/.NET background (where Code Contracts exist, and are awesome), I would absolutely love to have DBC in Rust.

[HunterGraubard]

I think this would be a great feature. One possible disadvantage I can think of with the libhoare library is... That would work for custom user code, but not for existing standard library code. With Microsoft's Code Contracts, for example, contracts have been written for a significant portion of the standard library. People can use the standard library without using contracts, but if they do care about and use contracts, they immediately get support on it from the standard library.

[ErichDonGubler]

After discovering this issue, I'd like to mention that I'm actually developing a D-inspired macro library called Adhesion that lets you use pre and post blocks in addition to a body block that contains function implementation. It's pre-1.0, and there's still some API changes planned (mainly renaming the D-inspired invariant block to something that better communicates what the block actually does), but it should work with the majority of fn definitions that don't use pub (which has already been fixed and is awaiting release).

Here's an example from the project README:

use std::i32;

contract! {
    fn add_one_to_odd(x: i32) -> i32 {
        post(y) {
            assert!(y - 1 == x, "reverse operation did not produce input");
        }
        body {
            x + 1
        }
        pre {
            assert!(x != i32::MAX, "cannot add one to input at max of number range");
            assert!(x % 2 != 0, "evens ain't appropriate here");
        }
    }
}

assert!(add_one_to_odd(3) == 4);
assert!(add_one_to_odd(5) == 6);
// use the galvanic-assert crate for expected panics
assert_that!(add_one_to_odd(2), panics);
assert_that!(add_one_to_odd(i32::MAX), panics);

[burdges]

Anyone considered "trait integration tests" as a step towards DBC? Right now, you could add macros that generate test code to test trait impls, but they must be called manually. If you wanted to enforce it, then you'd need something more:

pub trait Foo {
    fn foo(&self);
}

#[cfg(test)]
pub trait FooTester : Foo {
    #[cfg(test)]
    fn test_new() -> Box<Self>;
}

#[cfg(test)]
#[require_but_elsewhere]
impl<F: Foo> FooTester for F;

#[cfg(test)]
impl<F: Foo> F {
    #[test]
    fn do_foo_test() {
        let me = test_new();
        ...
    }
}

In this, the #[require_but_elsewhere] demands the impl exist but does not provide test_new itself. Also F::do_foo_test() is an inherent method for any Foo that only exists here and becomes a test.

You might need the #[test] to appear inside the FooTester sometimes trait too. I used Box<Self> here so that test_new need not be Sized, but maybe some use cases still need it, like tests in no_std.

[Ixrec]

@burdges I haven't seen that idea before, and it jumps out to me as the only "DBC" idea so far that might actually deserve to be a core language feature (this thread has always puzzled me since all of the concrete suggestions seemed just fine as a crate).

For now I suppose you can still get a meaningful proof of concept in a crate by simply requiring the client to put your magic test-generating macro in their test module. But the general idea that a library may want to "impose" (suggest?) tests on all of its client crates seems like something worth adding to https://internals.rust-lang.org/t/past-present-and-future-for-rust-testing/6354

[ghost]

Just a small comment on macro/lib/ language based solution for contract based programming. First i think everyone should read

http://joeduffyblog.com/2016/02/07/the-error-model/

it is a good blog about the issue.

Many thing can be done using lib level solutions, but I'd prefer the language level contract

• can be made part of doc and any IDE to show/display a pre/post condition of a function. It can be done for the lib version too, but if there are many non-official solution they will deverge.
• as compiler evolves it can be used to emit compile time errors and optimize code based on pre-conditions. Rust has made a really big progress toward safe codes and adding contrats could make it even safer. (And make it into mission critical systems one time)

[burdges]

Yes, I liked his explanation that contracts represent part of the type signature of a function, or presumably a type. I noticed he also recommended range types over contracts when possible, which likely means full refinement types in Rust's context.

[japert]

Hey, I just discovered this thread.
I am coming from a C++ background, where library-based contracts programming is still needed in the abscence of c++20.

What I read multiple times in this thread is the question:

What does libhoare not provide that a language-based feature could provide?

One thing that I see no way to do in library-based solutions is what @ErichDonGubler touches on
in the readme of his library Adhesion:

struct invariants.

D has an invariant keyword but even that is not strong enough.
If we have a container

struct Container{
  i32 size,
  i32 capacity
}

We'd want to express that size must be smaller or equal to capacity at all times such as:

struct Container{
  i32 size,
  i32 capacity
}
impl Invariant for Container{
  fn check(&self) -> bool {
     self.size <= self.capacity
  }
}

This runtime check should be executed at all times where size or capacity are written to.
To ensure this, we would really need some language support.
To do this in a library, one would need ugly wrapper types for size and capacity, which affect ergonomics and runtime performance.

[Ixrec]

I think you could do that in a library by expecting the user to put an attribute on each impl block that somehow describes the invariants. That obviously gets annoying if you have a lot of impl blocks for the same time, but AFAIK that's a pretty unusual case, and a pretty mild nuisance.

[NyxCode]

I have thought quite a bit about this, and I think the following would be a viable addition to rusts type system.

Imagine we've got a function divide(f64, f64) -> f64. It would panic if the second argument was 0, so we'd like to encode that into a contract. Conceptionally, this is similar to a where clause, so i propose this syntax:

fn divide(a: f64, b: f64) -> f64 
where b != 0.0 
{
    a / b
}

This could be something the type system enforces during compile time. For the function to be called, the compiler would require you to ensure that the precondition is actually met:

if b != 0.0 {
    divide(a, b);
}

More generally, I don't see why one couldn't use any pure expression in such a where clause. As far as I know, we can express such expressions with const fn.

Probably, we'd want an escape hatch to bypass these requirements at compile time. Maybe an annotation #[skip_contract] could move these checks to runtime.

[nixpulvis]

Probably, we'd want an escape hatch to bypass these requirements at compile time. Maybe an annotation #[skip_contract] could move these checks to runtime.

Why would you want to skip the checks? If these are to be thought of like types, then they must be upheld. Runtime checks might be how you get non-const functions however...

To me though, contracts are runtime checks. The idea of checking const equalities in the where clause seems more fitting to call static "guards", since they are much more like the match arm's guard than what I think a contract is anyway.

[NyxCode]

Why would you want to skip the checks? If these are to be thought of like types, then they must be upheld. Runtime checks might be how you get non-const functions however...

I think there will be cases where the compiler cannot completely ensure that a precondition is met. If that turned out to be the case, there would need to be a way to bypass it, i'd say.

To me though, contracts are runtime checks. The idea of checking const equalities in the where clause seems more fitting to call static "guards", since they are much more like the match arm's guard than what I think a contract is anyway.

I somehow don't feel runtime checks are not something which would fit into the language - Being able to ensure correctness at compile time is what makes me love rust.

Could you expand a bit on what the major difference to contracts would be here? Being able to put semantic requirements on arguments & return values of functions seems pretty close to what I understand contracts to be about.

[burdges]

We discussed #[test] in traits above, which makes some sense, and maybe doable now with custom test harnesses.

I'd suspect formal verification tools like static constraints for runtime values should live outside rustc itself, perhaps handling MIR though. If interested, you should probably explore doing a PhD with some suitable formal verification research team.

[nixpulvis]

@NyxCode I recommend you read a bit about both: dependent type systems and Racket lang's contracts. Specifically, contract blame is interesting in my opinion. I'll re-link this great paper on the subject here: http://www.ccs.neu.edu/racket/pubs/popl11-dfff.pdf

It seems to me you are looking for something more like a dependent type system, since your focus is on the static checking aspect of the system. With that said, these checks should not be able to be opt'd out of, just like you don't opt-out of an argument being an integer. Perhaps, it's better to think of them as refinements to the existing types... Anyway, there's a lot of academic research on these topics, no doubt.

[indolering]

I'd just like to chime in with my support for this. Coming from a C#/.NET background (where Code Contracts exist, and are awesome), I would absolutely love to have DBC in Rust.

Code Contracts in C# are dead, the implementation burden was too high and they have been converted into no-ops. However, C#'s Code Contracts were a poorly designed imitation of DbC that didn't integrate with the rest of the language and simply ignored failure recovery. IMHO, C#'s Code Contracts was just Microsoft Research justifying it's existence by shoehorning some of its work in to C#.

@Ixrec RE: Why can't you just use a library?

DbC enriches a function's API contract beyond the type signature. You could use a validation library, but that's like arguing duck typing is a valid substitute for static typing. It's possible to get equivalent levels of safety and correctness, but it requires a lot of extra time and effort. Joe Duffy gives a good overview of the problems with imperative "contracts".

To me though, contracts are runtime checks.

Only because most programming languages lack a proof system, so everything has to be a runtime check. In languages that support verification, I believe assert, ensures and invariant contract clauses are traditionally treated as compile time checks. Dafny, for example, uses expect for runtime checks.

The idea of checking const equalities in the where clause seems more fitting to call static "guards", since they are much more like the match arm's guard than what I think a contract is anyway.

This seems counter-intuitive to me, because if I can prove something won't happen I don't need to hire a guard to prevent it from occurring. We could introduce disprove as a way to trigger a compile-time error when static analysis can find issues, but use runtime checking if static analysis can't prove the assertion to always be true.

You really do need to have support for specifying both compile-time and runtime assertions, however, as this impacts the modularity of the verification system.

[nixpulvis]

I'll just quote an earlier post of mine here:

Contracts are by design runtime checks that generally fit outside the type system of the language your in. You can even think to write weird contracts like one that ensures a function is only called after 6PM and before 8PM.

Of course the more you can validate statically, the better. Contracts (as I view them) fill in the rest with a uniform and powerful runtime semantics. Perhaps some form of gradual typing is what you are after, since you can treat that which is static and that which isn't similarly, and leave some things unspecified... and leaves you with a single (more complex) type system. However, I have no idea what this means for Rust specifically. It also seems like a much larger departure from the language as a whole.

With that said, I'm not personally sure what the goal of this issue is exactly, since "contracts" and design by contract seems to have so many different ideas behind it. If it's just a matter of writing a crate (or using the existing ones), what exactly is stopping adoption? If there is some language level support needed, what would that be?

I hinted at using where to embed more expression constraints, but I would be somewhat surprised if anyone actually wants runtime checks in there as @indolering addressed above. My only point was that we already place guards very close to more static things like de-structuring, perhaps this isn't quite as crazy as it might seem.

[indolering]

Contracts are by design runtime checks that generally fit outside the type system of the language your in. You can even think to write weird contracts like one that ensures a function is only called after 6PM and before 8PM.

Of course runtime checks are useful, assume is useful if your verification condition contains a^n + b^n = c^n. But it's a mistake to limit contracts to either runtime or compile time checking.

Perhaps some form of gradual typing is what you are after

I mean, that's required to get the annotation overhead to acceptable levels. But straight-up compile-time assertion clauses (without inference based on the body of the code) are necessary to keep verification modular.

With that said, I'm not personally sure what the goal of this issue is exactly, since "contracts" and design by contract seems to have so many different ideas behind it. If it's just a matter of writing a crate (or using the existing ones), what exactly is stopping adoption? If there is some language level support needed, what would that be?

I can think of a few items that would make experimentation easier, like named return variables and reserving quantifier keywords. However, it would probably be best if this ticket were closed and discussion moved to the forum or a working group until someone can propose some concrete steps. Right now it's just a grab bag of DbC concepts and "me too" posts.

I would be somewhat surprised if anyone actually wants runtime checks in there as @indolering addressed above.

The motivation for disprove is ergonomics, but it's off-topic 😛.

I mainly wanted to to note that C# Code Contracts are now dead, largely because the bolt-on nature of the implementation limited their utility. If we want to use Rust to build high-assurance systems, we will need to enrich the API contract beyond basic type checking and simple validation libraries.

[SOF3]

I understand that assertions on external environment need to have a standard way to declare, but I don't understand why checks on parameters can't be fully fulfilled by type system. Isn't NonZeroU32 much more self-explanatory than whatever macro magic that checks x > 0?

[indolering]

I understand that assertions on external environment need to have a standard way to declare, but I don't understand why checks on parameters can't be fully fulfilled by type system. Isn't NonZeroU32 much more self-explanatory than whatever macro magic that checks x > 0?

Null checking and range checks represented the bulk of C# contracts and ~90% of contracts in Midori, which are more ergonomically handled using specialized types. However, you run into limitations with proliferation of incompatible types and expressing relations between parameters, such as expressing x < array.len().

But also ... this thread isn't an intro to contract programming 😸.

[matu3ba]

I have not seen anything concrete, so here is a general overview of stuff we could do with my opinion.

I dont understand, why anyone would want to have a language-specific feature that is not usable with external proof engineering tooling.

1. Rust has the most advanced static analysis in-build with the borrow checker. However it is not annotated as comments, which is a pain then to extract with external tooling for better analysis how memory is used, pointer analysis etc. Fixing this would mean redundancy. And yes, parsing MIR is harder than a well-defined standard in source code and one wants to support multiple languages with the tooling.
2. We can try to build formula generation from annotation and extraction to Isabelle, which is completely out of scope and nobody sane does it. Its way easier to use cogent or something like that to generate C code and use compcert.
3. We can try to build dynamic analysis, which boils down to Value Set Analysis or other numeric representations, which are plentiful. This includes so many numeric representations that we will likely never agree on one.
4. We can have SMT or SAT analysis for incremental verification and regression verification and there is already the very nice SMT-lib standard. The annotation is however not human-friendly readable (prefix notation aka polish notation), so we would either want a converter tool for the SMT solver or link to the respective source code in another document (and display an human-friendly overlay).

A contract on itself is just a formal model for behavior, for where I know 3 general automatically checkable models with increasing difficulty: 1. specification automata, 2.LTL formula and 3.CTL formula.

I dont think a Rust-specific solution scales and using a proper standard would improve the state of the art significantly. C-solutions have the same problems that tooling cant be generated without some standard to rely on. So tooling usabilty does not improve, because you can not swap the tool.

[burdges]

I'd suggest exploring hacspec (github) if interested in this topic:

Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust by Denis Merigoux, Franziskus Kiefer, and Karthikeyan Bhargavan at PROSECCO, Inria de Paris (via)

[burdges]

There is also a pattern in #3095 (comment) that looks doable from procmacros.