> 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 "significa

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