3 ms·

I think you are not using 'proof' in the way that most people would understand it. A proof is usually considered a series of steps someone can take to verify th

I think you are not using 'proof' in the way that most people would understand it. A proof is usually considered a series of steps someone can take to verify that something is true themselves (i.e. there is no need to trust whoever produced the proof is malicious or mistaken about what they are trying to prove, if you can follow the proof you can see for yourself). Proving something to a compiler therefore is generally understood to mean giving something to the compiler which it actually checks it sound (even if it could not produce the proof on its own). This is effectively how type-checking and borrow checking works (your program is a kind of proof the compiler verifies). 'unsafe' in this case is not a proof, it is more like a promise (not in the async sense) or assertion (not in the debug sense). The compiler trusts that you have not made a mistake, it does not have any way to verify that you haven't. You may have a proof to the person reading the code that there is no mistake (or you may not, either because your proof is incorrect or the person cannot understand the proof), but it is not a proof to the compiler. (In fact, there was much bikeshedding at one point about renaming the 'unsafe' keyword to make this explicit: suggestioned included 'assumed_safe', 'trustme', 'trusted', as well as less serious ones like 'yolo' and 'hold_my_beer_and_watch_this': https://github.com/rust-lang/rfcs/pull/117 https://github.com/rust-lang/rfcs/pull/117)

volta83 5y ago
> I think you are not using 'proof' in the way that most people would understand it. I have corrected many math exams of students over the years. A "significant" amount of the "proofs" provided by the students in those exams were wrong in one way or another. Many students continued the exams under the assumption that what they just incorrectly proved, was actually correct. They had no way to verify whether they proofs were correct or not. No theorem provers were allowed in the exam. Yet all of them called what they wrote "a proof". --- This is pretty similar to how Rust works. Without unsafe, Rust proves your programs sound for you. Unsafe let's you supply your own soundness proofs for parts of the program that the compiler does not know how to prove (or disprove). If the proofs are not correct, RUst makes no guarantees. The claim that because "Rust does not prove these for you, they are not proofs" is unfair. That's like claiming that any "proof" that has not been proved in a theorem prover does not deserve to be called "a proof". I respect your way to see this. I just don't see it this way.

volta83 5y ago

> I think you are not using 'proof' in the way that most people would understand it. I have corrected many math exams of students over the years. A "significant" amount of the "proofs" provided by the students in those exams were wrong in one way or another. Many students continued the exams under the assumption that what they just incorrectly proved, was actually correct. They had no way to verify whether they proofs were correct or not. No theorem provers were allowed in the exam. Yet all of them called what they wrote "a proof". --- This is pretty similar to how Rust works. Without unsafe, Rust proves your programs sound for you. Unsafe let's you supply your own soundness proofs for parts of the program that the compiler does not know how to prove (or disprove). If the proofs are not correct, RUst makes no guarantees. The claim that because "Rust does not prove these for you, they are not proofs" is unfair. That's like claiming that any "proof" that has not been proved in a theorem prover does not deserve to be called "a proof". I respect your way to see this. I just don't see it this way.