Can rustc prove this? [ proposal ]

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.

3 Likes

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

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.

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

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