# Can rustc prove this? \[ proposal \] **URL:** \ **Category:** compiler\ **Created:** [May 27, 2020, 6:20pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443 "2020-05-27T18:20:07Z")\ **Posts on this page:** 20\ **Page:** 1
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 27, 2020, 6:20pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/1 "2020-05-27T18:20:08Z")
```rust fn add(a: i64, b: i64) -> i64 { a - b } ``` **proposal** : perform analysis of identifiers and comments to match with their implementation. ---
**Author:** ![steffahn](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/steffahn/32/13288_2.png) [@steffahn](https://internals.rust-lang.org/u/steffahn)\ **Post date:** [May 27, 2020, 6:39pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/3 "2020-05-27T18:39:44Z")
I’m afraid that what you’re proposing is either impossible or not too useful, depending on the scope you’re imagining. Ordinarily you wouldn’t ever be re-implementing addition on machine integers, so special analysis from the compiler on cases that don’t get far beyond your example might be fairly useless to people building real-world Rust applications. If you think of a larger scope on the other hand, then you must be careful not to over-estimate the “intelligence” of a computer, or a compiler in particular. What I can tell from your (by the way a bit too short) “proposal” is that you’re asking about a compiler checking properties/correctness of a program. When we’re talking about arbitrarily complex properties we’re quickly hitting even the theoretical boundaries of what computers can automatically proof. Also you’re suggesting for the compiler to look into comments and names of identifiers. It almost sounds like you would expect the compiler to understand the English language, or somehow guess what the developer had in mind, two things that computers in general are, as of now, not really capable of doing at-all. * * * Something that is possible however is for computers to check correctness properties of programs that are formally specified by the programmer in some way and where potentially even some form of proof is given. In the context of Rust this is what the type system is for. You could interpret the situations where you’re fighting with the borrow checker as refactoring your program to (implicitly) give some proof that you’re doing things correctly around Rust’s ownership semantics. Type systems can go way further though, I’m afraid this is not something that will come to Rust anytime soon, but if you search the internet for “automatic theorem proving” of “proof assistants” or in particular “dependent types” you might find some material on this kind of topic in the meantime. ---
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 27, 2020, 7:10pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/4 "2020-05-27T19:10:46Z")
in order to make rust safe, i think in future rustc should do something like this. ---
**Author:** ![notriddle](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/notriddle/32/14082_2.png) [@notriddle](https://internals.rust-lang.org/u/notriddle)\ **Post date:** [May 27, 2020, 7:16pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/5 "2020-05-27T19:16:56Z")
It sounds like you're asking to implement General AI in the rust compiler, which just isn't going to happen. ---
**Author:** ![samsieber](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/samsieber/32/4671_2.png) [@samsieber](https://internals.rust-lang.org/u/samsieber)\ **Post date:** [May 27, 2020, 7:33pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/6 "2020-05-27T19:33:58Z")
The closest thing you could do to this would be some sort of tool that searches for implementations of the same function signature (name, args and output), and compares yours to them. It would have to be an external tool though. ---
**Author:** ![Tom-Phinney](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/tom-phinney/32/3299_2.png) [@Tom-Phinney](https://internals.rust-lang.org/u/Tom-Phinney)\ **Post date:** [May 27, 2020, 7:49pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/7 "2020-05-27T19:49:39Z")
Personally, I find that comments are most useful when they summarize what the code is doing, rather than describing it point-by-point in exquisite detail. (Aside: Many of us have reviewed human-written assembler code that does the latter.) If the comments are a summary that abstracts over the details, it's likely impossible for even advanced AI to prove that the summarization is accurate. ---
**Author:** ![kennytm](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/kennytm/32/161_2.png) [@kennytm](https://internals.rust-lang.org/u/kennytm)\ **Post date:** [May 27, 2020, 7:51pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/8 "2020-05-27T19:51:12Z")
If I'm implementing a GF(2N) type I would implement `add()` using XOR, and that is totally expected. Is there a real-world example leading to this proposal? ---
**Author:** ![josh](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/josh/32/5934_2.png) [@josh](https://internals.rust-lang.org/u/josh)\ **Post date:** [May 27, 2020, 7:53pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/9 "2020-05-27T19:53:54Z")
I've seen compilers that lint when the implementation of a trait uses an unexpected operator. And I could also imagine a lint like "you've implemented two traits expected to be distinct but they have the same implementation", to catch copy-paste issues. But beyond heuristics like that, this isn't solvable. ---
**Author:** ![Aloso](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/aloso/32/5039_2.png) [@Aloso](https://internals.rust-lang.org/u/Aloso)\ **Post date:** [May 27, 2020, 11:01pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/10 "2020-05-27T23:01:46Z")
IntelliJ has a "suspicious variable/parameter name combination" warning to detect e.g. when you pass a variable `x` as a parameter named `y`. This also works if the variable name just contains an `x`, e.g. `xCoordinate`. By default, the following groups are defined: - x, width, left, right - y, height, top, bottom Combining names from different groups triggers the warning. You can also add more groups. A more thorough lint could also check e.g. if parameters are passed in the correct order, based on the variable names: ```rust fn f(foo: bool, bar: bool) {} let foo = true; let bar = false; f(bar, foo); ``` ---
**Author:** ![cuviper](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/cuviper/32/1897_2.png) [@cuviper](https://internals.rust-lang.org/u/cuviper)\ **Post date:** [May 27, 2020, 11:14pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/11 "2020-05-27T23:14:01Z")
Clippy kind of does this -- not trying to guess your intent for _arbitrary_ methods, but it will warn if you subtract in `impl Add`. [https://rust-lang.github.io/rust-clippy/master/#suspicious\_arithmetic\_impl](https://rust-lang.github.io/rust-clippy/master/#suspicious_arithmetic_impl) ---
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 28, 2020, 6:19pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/12 "2020-05-28T18:19:17Z")
i think instead of putting this to the compiler, it should be implemented as a part of a static analyzer. ---
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 28, 2020, 6:22pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/13 "2020-05-28T18:22:32Z")
> [@steffahn](#): > > ’m afraid that what you’re proposing is either impossible why it is impossible. human went to moon on 1969. 1969! now we are at 2020 and we can't build a software system that can do this. why? ---
**Author:** ![steffahn](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/steffahn/32/13288_2.png) [@steffahn](https://internals.rust-lang.org/u/steffahn)\ **Post date:** [May 28, 2020, 6:30pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/14 "2020-05-28T18:30:51Z")
And already in 1936, Alan Turing proved that automatic software analysis tools are fundamentally limited (halting problem). That was way before computers even existed. Sometimes "impossible" doesn't refer to the fact that humanity hasn't achieved something yet but instead means that something is _actually_ impossible. ---
**Author:** ![HerrJemine](https://avatars.discourse-cdn.com/v4/letter/h/7ba0ec/32.png) [@HerrJemine](https://internals.rust-lang.org/u/HerrJemine)\ **Post date:** [May 28, 2020, 8:01pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/15 "2020-05-28T20:01:55Z")
To be fair, you don't need to solve the halting problem for this. You _merely_ need general human level AI. Totally doable! The Rust 2121 edition should definitely have this. 😉 ---
**Author:** ![Aloso](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/aloso/32/5039_2.png) [@Aloso](https://internals.rust-lang.org/u/Aloso)\ **Post date:** [May 28, 2020, 10:51pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/16 "2020-05-28T22:51:14Z")
The purpose of the compiler is just to compile a program. It's purpose is _not_ to prove that the program is semantically correct, you should use **clippy** for this. Clippy lints don't require an edition boundary, so you can implement this feature if you want 😉 ---
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 28, 2020, 11:36pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/17 "2020-05-28T23:36:57Z")
yes, i think this should be implemented on clippy. ---
**Author:** ![jhpratt](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/jhpratt/32/11640_2.png) [@jhpratt](https://internals.rust-lang.org/u/jhpratt)\ **Post date:** [May 28, 2020, 11:41pm UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/18 "2020-05-28T23:41:32Z")
Without being 100% clear on _what_ you're exactly proposing, clippy already has a lint similar to the example in the original post, as has been mentioned. ---
**Author:** ![notriddle](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/notriddle/32/14082_2.png) [@notriddle](https://internals.rust-lang.org/u/notriddle)\ **Post date:** [May 29, 2020, 1:42am UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/19 "2020-05-29T01:42:47Z")
> [@milrope](#): > > why it is impossible. human went to moon on 1969. 1969! now we are at 2020 and we can't build a software system that can do this. why? If someone is voicing concerns about your proposal, please don't just brush them off. If you think it's possible, give actual reasons. What would a system that recognizes the bad code patterns you want to prevent actually look for? Does the system you're thinking of try to prove the equivalence of arbitrary English with code? If not, then what does it do instead? ---
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 29, 2020, 7:43am UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/20 "2020-05-29T07:43:26Z")
my post is just a example of a case. I am talking about all possible issue that can happen. and lint them all to prove that the implementation is 100% correct. ---
**Author:** ![milrope](https://avatars.discourse-cdn.com/v4/letter/m/d9b06d/32.png) [@milrope](https://internals.rust-lang.org/u/milrope)\ **Post date:** [May 29, 2020, 7:49am UTC](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443/21 "2020-05-29T07:49:31Z")
> [@notriddle](#): > > Does the system you're thinking of try to prove the equivalence of arbitrary English with code? yes something like that. It has to prove that the implementation is correct by analyzing all the information it has been given. identifiers and comments. if they don't match, that will result to an error. [Next page](https://internals.rust-lang.org/t/can-rustc-prove-this-proposal/12443.md?page=2)