You did mention uninitialized arrays but uninitialized data is inherently unsafe. It's not an operation that can be made safe.

Sure it can. You just need primitives which can be used in asserts such as

    is_initialized(tab,i,j)

indicating that an array is initialized within those limits. Then you can write asserts such as

    assert(is_initialized(tab,i,j-1));
    ... initialize tab[j]
    assert(is_initialized(tab,i,j));

Standard program verification technology. Verification of unsafe sections is a useful goal, and deserves language support. Hand-waving about "encoding the invariants specific to your use case in your code" is insufficient. You need to write them down and prove them. Then you can eliminate them from the run-time code.

You want us to add dependent types to Rust (which is what you just proposed)? Half the time I see you complaining about Rust you're complaining that it's too complicated!

> You just need primitives which can be used in asserts such as

Sounds like you're going along the path of a dependent type system (in this specific case)? Yes, that could be done, and would perhaps let you reduce a couple of unsafe blocks in the implementation of Vec and other buffer-based abstractions (but not get rid of all of them).

FWIW there is active work going on for formal verification of Rust (both safe and unsafe code), in the RustBelt project.

In general making unsafe blocks run formal verification would be an interesting thing to do (and would solve this problem completely). I don't think it deserves language support, however (nice-to-have, not must-have). This is a very different goal from your original point of adding a few language features that ease writing lower level abstractions.

--------

Ultimately, you're right. While pcwalton did mention "There's no way to solve that problem without just forbidding unsafe code entirely."; this is a possible alternative -- have language support for scoped formal verification that allows you to use "unsafe" operations safely. I think this is an extreme solution to what I consider to be a mostly nonexistent problem.

For really security sensitive code this would indeed be very useful (and is probably a big motivator behind the RustBelt project). Or just use SPARK or something.

But for most Rust users I think the current system is pretty robust and provides enough primitives to write clean, easy-to-verify abstractions with (verifiable) safe API boundaries. (when I say "verify" here I mean it in the informal sense). I haven't come across unsafe code doing contortions, and I have had the (mis?)fortune of going through a lot of unsafe code. The only rough edges are with FFI, and these are mostly due to a lot of things about unsafe code being underspecified (which don't crop up as often in pure rust unsafe code, but do crop up when you through some C/++ FFI in the mix). There is active work on specifying the exact semantics of unsafe code however, so that should be fixable once it happens.

Don't forget there's a middle ground between not having them and manual, formal verification. It started with Eiffel with basic contracts that checked properties during testing and/or runtime. That did well in commercial deployments. SPARK took it formal with a basic, boolean encoding for programmer understanding. It uses a subset of Ada to prove absence of all kinds of error conditions without runtime checks or manual proof. It can optionally do more with a theorem prover but optional. Eschersoft did Perfect Developer to do it in high-level language with C, Java, or Ada generation. So, at least three are doing it in products with industry deployments with two highly concerned about performance in low-level applications.

Although I'm not getting into this dispute, I will add in general that Rust might benefit from such contracts or push-button verification of key properties as deployed successfully in Eiffel, SPARK, Ada 2012, and Perfect Developer. A language subset might be used like in SPARK to allow automated verification of those sections against common types of errors. Three follow-up benefits will be easier changes/integrations in maintenance phase, automated test generation from specs, and aiding dynamic analysis by giving it invariants to look at. Could be optimization benefits but I'm not qualified to say on that. Intuitively seems possible like using minimum-sized, data structure for a number range in spec or type. Stuff like that.

These techniques are really under-utilized despite being proven out many times over in high-reliability products.

Yeah, this exists, and would be interesting. I again think that it's a bit too extreme a solution to be baked into Rust itself, but I'd love a SPARKish Rust variant.

I'd like both. SPARK's stuff was ported to Ada 2012. It can be done for Rust as well. The trick is to make it optional so people don't have to pay attention to it. Maybe even have editors filter it out for people not paying attention to it. At the least, it being used in standard library and OS API's would let it enforce correct usage of those in debug/testing mode. 80/20 rule says that should have some impact given how much damage we've seen C and Java developers do misusing the foundational stuff.

Yeah, me too. However, I think we should wait for the formal verification of Rust to be completed before trying this. While it is possible to make something SPARKish without complete formal verification, it's probably better to build it using concepts learned during the formal verification.