Can rustc prove this? [ proposal ]

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.


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?


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.


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:

fn f(foo: bool, bar: bool) {}

let foo = true;
let bar = false;
f(bar, foo);

Clippy kind of does this -- not trying to guess your intent for arbitrary methods, but it will warn if you subtract in impl Add.


i think instead of putting this to the compiler, it should be implemented as a part of a static analyzer.

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?

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.


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. :wink:


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 :wink:

yes, i think this should be implemented on clippy.

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.

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?


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.

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.

What issues, then? Just saying "all possible issues" doesn't help if you want something implemented.

And keep in mind that, as others have mentioned, 100% correctness is simply infeasible. How do you propose to get concrete information out of comments? Identifiers? That would be a good starting point.

okay, may be 100% correctness can't be proven. but large amount can be proven.

okay. I want a neural network that can read and write correct English and Rust code. And verify the implementation with the surrounding information.

Is this complicated? we now have a lot of peer reviewed rust code. So i think training a system isn't hard.

May be this can be implemented to a separate program. someone in the community needs do this.

may be the rust analyzer guys will do this.

I want this. no matter how hard this is.

Yes, that is incredibly complicated, which is why nothing like that exists for any language that I'm aware of.

Are you offering up a significant portion of your time? Don't offer up other people's time — that's rude and inconsiderate at best. You can start design and implementation of you want it so badly.


okay. I want a neural network that can read and write correct English and Rust code. And verify the implementation with the surrounding information.

Is this complicated? we now have a lot of peer reviewed rust code. So i think training a system isn't hard.

Well, luckily this neural network exists! And it usually takes only about 22 years and a lot of diapers to train it to a reasonable accuracy. But of course it still makes occasional errors, so you should use an ensemble model.