Our great sponsors
-
-
creusot
Discontinued Creusot helps you prove your code is correct in an automated fashion. [Moved to: https://github.com/creusot-rs/creusot] (by xldenis)
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
It is perfectly reasonable that `from_utf8_unchecked` is unsafe because the sequence of operations `from_utf8_unchecked(array).chars().next()` will call [1] and can trigger memory unsafety with the `unwrap_unchecked` call if the array is not valid utf-8. This means that at least one of the three functions must be marked unsafe.
[1] https://github.com/rust-lang/rust/blob/027a232755fa9728e9699...
I’m doing my PhD on the formal verification of Rust, and while you’re right that safe code provides a lot of informal advantages it also dramatically simplified form reasoning.
In particular, the dirty secret of C verifiers is that they don’t handle pointers all that well. Either you find yourself doing a lot of manual proof work or you have to dramatically simplify the memory model.
In contrast, when verifying safe Rust, the rules of the borrow checker allow us to dramatically simplify the verification work. All of a sudden verifying a manual memory program with pointers (borrows) becomes as simple as verifying a basic imperative language. I’ve been working on a tool: https://github.com/xldenis/creusot to put this into practice
On the other hand, the moment you dive into unsafe, all bets are off and you find yourself wading through the marshes of (weak) memory models with your favorite CSL as your only friend.
I’ll be even lazier (heh) and just straight up leak memory for true once-set read-only config values.
https://github.com/shepmaster/stack-overflow-relay/blob/273a...