fn add(a: i64, b: i64) -> i64 {
a - b
}
proposal : perform analysis of identifiers and comments to match with their implementation.
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.
7 Likes
in order to make rust safe, i think in future rustc should do something like this.
It sounds like you're asking to implement General AI in the rust compiler, which just isn't going to happen.
4 Likes
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.
1 Like
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.
4 Likes
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?
5 Likes
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.
5 Likes
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
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
10 Likes
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.
17 Likes
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. 
3 Likes
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
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?
5 Likes
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.