Design By Contract #1077
Comments
|
I don't know much about this, but is this related: https://github.com/nrc/libhoare Also, we're not post-1.0 yet :) |
|
The beta is not considered post-1.0? |
|
Post 1.0 is after May 15th, when the real 1.0 is out. |
|
DBC looks like one of these things that should be a syntax extension. |
|
@arielb1 I disagree. Syntax extensions have no access to type resolved results. I believe what one would actually want would be a compiler plugin. |
|
@DiamondLovesYou I thought syntax extensions and compiler plugins were the same thing. Can you give an example of each? |
|
@gsingh93 I edited the tense in the original post. @DiamondLovesYou I would also like an example of each. |
|
@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. |
|
Anyway, what is design by contract? Rust has a powerful type system that already handles the 90% most popular propositions. |
|
I mean, the Rust type-system covers at least:
And that's at least 80% of all propositions already. |
|
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.
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. |
|
@KingOfThePirates Can you look at |
|
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)? |
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. |
|
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? |
|
@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. |
|
@Diggsey Oh, thank you :) |
|
@nrc Thank you for your time and consideration. Looks like we must listen to what nrc said on this matter.
Rust gods: Please make sure to consider libhoare's wish list when making these "medium term future" syntax extension changes:
Edit 1 (Wednesday, April 22, 2015):
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. |
|
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. |
|
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 |
|
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. |
|
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. |
|
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 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 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. |
|
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. |
|
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). |
|
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. |
|
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. |
|
@Jragonmiris Proofs look interesting. Might not solve the same problems Design By Contract solves, but it looks like it can be useful. |
|
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 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. |
|
A potential challenge is that Rust doesn't really have any notion of purity. Something like If I may suggest a problem of a perhaps more limited scope: proving that |
|
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. |
|
@socumbersome what would you provide that isn't already in https://github.com/nrc/libhoare? |
|
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:
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. |
|
@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:
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 @gsingh93 - if we talk about DBC without PS and agree on separation of those, then in |
|
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. |
|
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. |
|
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. |
|
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 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); |
|
Anyone considered "trait integration tests" as a step towards DBC? Right now, you could add macros that generate test code to test trait In this, the You might need the |
|
@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 |
|
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
|
|
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. |
|
Hey, I just discovered this thread. What I read multiple times in this thread is the question:
One thing that I see no way to do in library-based solutions is what @ErichDonGubler touches on struct invariants. D has an struct Container{
i32 size,
i32 capacity
}We'd want to express that 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 |
|
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. |
|
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 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 Probably, we'd want an escape hatch to bypass these requirements at compile time. Maybe an annotation |
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 |
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.
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. |
|
We discussed 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. |
|
@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. |
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".
Only because most programming languages lack a proof system, so everything has to be a runtime check. In languages that support verification, I believe
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 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. |
|
I'll just quote an earlier post of mine here:
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 |
Of course runtime checks are useful,
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.
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.
The motivation for 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. |
|
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 |
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 But also ... this thread isn't an intro to contract programming 😸. |
|
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.
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. |
|
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) |
|
There is also a pattern in #3095 (comment) that looks doable from procmacros. |
and others
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.
So, when do you think official Rust-supported DBC solutions should be discussed?
The text was updated successfully, but these errors were encountered: