Can rustc prove this? [ proposal ]

compiler
#10

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);
2 Likes
#11

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

9 Likes
#12

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

#13

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?

#14

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.

16 Likes
#15

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:

2 Likes
#16

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:

#17

yes, i think this should be implemented on clippy.

#18

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.

#19

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?

5 Likes
#20

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.

#21

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.

#22

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.

#23

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

#24

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.

#25

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.

3 Likes
#26

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.

15 Likes
#27

Heuristics like this exist in some linters.

E.g. people from PVS-Studio C/C++ linter described in one of their (too many) blog posts how they catch mistakes happening in practice due to developers copy-pasting code and forgetting to update the copy-pasted version using any source code information available as input.

Which is very similar to your case:

fn add(a: i64, b: i64) -> i64 {
    a + b
}

fn sub(a: i64, b: i64) -> i64 {
    a + b // Oops, copypasted from add, forgot to update
}

As for machine learning, people likely use it for linting too.
At least I've heard about attempts to do in the Svace Static Analyzer for C/C++/Java used in Samsung.

Now milrope only need to convince clippy maintainers to work on something like this.
Which is unlikely because he seems to be a troll account.

#28

I don't think you understand just how hard this problem really is. First, study the Halting Problem and Undecidability. Taken together, this proves that you cannot do what you're asking for in general. At best, you can come up with a large number of extremely specific tests, which is pretty much what clippy does.

But your suggestion of having an automated system that reads the comments to learn the intent of the programmer, and then verify that the intent matches the code... I do not have the vocabulary to sufficiently explain how hard a research problem that is. What you've just described is pretty much the Holy Grail of AI research (beating the Turing test); it may even be harder than that (I have no idea if that's so or not; is there a complexity class beyond 'undecidable'?).

Someday we might have something like an 'expert programmer in a box' (which is what you're asking for), but if we do, I don't expect it for at least a few hundred years. That's how difficult what you're asking for really is.

5 Likes
#29

Locking this because it isn't really providing any more actionable feedback. If the OP is serious about working on this, adding to or improving Clippy’s heuristics is probably a good starting point. Please open a new thread if you have more concrete questions or info about that, though please don’t come into this forum telling other people what they need to do.

9 Likes