Going on a tangent, but I honestly think 'unsafe' might suffer from a naming issue. It should've been called 'unchecked' or 'unverifiable' or something that says the code is merely not verified to be safe, not that it is actually unsafe.
C# tackled this problem 15 years ago. I'm sure other languages (Haskell) did it even earlier. When to use unsafe is a judgement call. Each developer and team will have to set their own standards. Some people will abuse it. None of this is new. At first it scares people. They think this is the brave new world, using unsafe feels gross and backwards! Eventually they understand where it is and isn't appropriate.
You might think "so what? Why even bother with a safe-by-default language?"
Because it greatly restricts the problem space. Rather than being forced to examine every line of code for every possible bit of undefined behavior or every path of flow control for memory errors you only need to think really hard about edge cases inside the unsafe blocks. Simply by virtue of being a relatively small number of blocks of few lines the problem of safety and correctness becomes easier to understand. Easier to test. Easier to reason about.
Unsafe is a tool. It's a dangerous tool so you should always wear your gloves and safety goggles. But when faced with a problem for which it is the best tool you should use it without regret.
If 95% of your code touches the other 5%, then that 5% is probably pretty important and useful and hopefully fast. Spending some extra time to verify safety in exchange for speed/control is a small price to pay, and will pay dividends from the other 95% of code that doesn't have to be inspected so closely.
Rust gets much inspired by C++ and seeks to be a systems language where " there should be no room for a lower-level language between [it] and native machine code".
If you want that, you need unsafe blocks. The intent is to use those blocks to build safe abstractions that can be used for the lion's share of your program.
I hadn't heard this before, and I love it! This seems like a very nice way to define what a systems programming language is. :-)
There are two things I consider necessary for that. First, that the Rust compilers become smarter in proving the safety of things by themselves. Second, that the Rust compilers become capable of verifying proofs given to them that show the safety of a given piece of code the compilers can't prove as safe on their own.
Let me restrict it to the faintly weaker "I hope we don't settle for unsafe being okay forever where we can prove safety".
I also imagine that it isn't allowed when using Bitcode deployment on iDevices.
However, I honestly feel that the Rust language itself isn't really the right language to be doing these kinds of proofs in. I think that the right language to do the actual formal verification in is likely to be something closer to Coq. Whoever undertakes this effort would probably use an automated theorem prover to prove the unsafe Rust code correct, like was done for seL4 using Isabelle.
You can think of this setup as offering a sort of layered verification: once the small core of code (the unsafe code in the standard library and popular crates, say) is proven correct, the type system and borrow checker effectively prove the rest to be memory- and thread-safe. In fact, that's what would make this system practical: most programmers wouldn't have to understand anything about the complexities of the theorem prover. They would get the benefit of verified memory- and thread-safety for free just by learning Rust.
We don't need to verify every single occurrence of unsafe, but whenever unsafe is necessary I feel the lack of some other guarantee holding our back.
Having optional small-scale(!) verification in Rust would be awesome.
Using other theorem provers has the same problems as when one tries to establish tools for checking memory safety in C: it isn't the default, just an addon.
In my eyes, there is a scale of verification-readiness in which Rust can position itself. The least ready would be having it completely separate and done by other tools in other files, the most ready would be having syntax for it in the language, having it in the same files, and checked by the standard compiler.
I think every bit of verification-readiness Rust has by default will have a strong effect that we can't achieve through other means.
Maybe, some things don't impact those not interested in verification. Say, have next to 'safe' and 'unsafe' also the 'verified' environment that also contains proof language as a core part of Rust. That way all ordinary code is still valid and everyody is free to use Rust without verification in mind.
Any ideas what could be done to make Rust verification-readier?
Depends on how you interpret the name—whether it's referring to what it does (makes things no longer automatically safe), or whether it's referring to what the code inside it does.
If you write only safe code, inside an unsafe{} block, then nothing unsafe is happening. Fewer compile-time static-analysis checks are happening, but if you manually verify that the code is "safe anyway" the way C/C++ programmers are forced to do, then you can declare that the code is safe, maybe with a comment like:
// this is safe
unsafe{ ... }
// this is safe
unchecked{ ... }
Section 8, UNSAFE mode
http://public.support.unisys.com/aseries/docs/clearpath-mcp-...
Is it possible that the link to personal safety of the terminology is what provides the best positive connotation in terminology but also causes this unwanted ambiguity in negated interpretation? If so, that's an annoying catch-22...