Undefined Behaviour as usual

Posted Feb 24, 2024 13:49 UTC (Sat) by mb (subscriber, #50428)
In reply to: Undefined Behaviour as usual by vegard
Parent article: Stenberg: DISPUTED, not REJECTED

What are you going to compute with your Rust program, if it doesn't include a single unsafe block?
You can't do I/O.

If you are going to rewrite and recompile your Rust program each time the input changes, then the Compiler is part of your program flow. The compiler is the "unsafe-block" in this case, which provides the input data. Without it, the Rust program can't process anything. It would be static.

Yes, we can have fully safe languages like Rust. But they must *always* interface to an unsafe part. Otherwise they can't produce results. Safe-Rust alone is useless. General purpose languages will always have an interface to unsafe code.

The real world is unsafe. The real world has UB.

Undefined Behaviour as usual

Posted Feb 25, 2024 0:55 UTC (Sun) by tialaramex (subscriber, #21167) [Link]

To be fair if you're willing to give up generality you can have software with excellent performance and no undefined behaviour. That's the point of WUFFS. We can and should write a lot more software in such languages (starting with, we should use WUFFS everywhere it's appropriate)

Generality is of course a price we cannot often afford. You wouldn't write the WUFFS compiler in WUFFS (the current transpiler is in Go) or an operating system, or indeed a web browser but the point is that our industry got into the habit of using chainsaws everywhere because they're so powerful, rather than using the right tool for the job.

Undefined Behaviour as usual

Posted Feb 26, 2024 7:50 UTC (Mon) by NYKevin (subscriber, #129325) [Link] (2 responses)

In principle, it is possible to compose a complete, usable system entirely out of a combination of:

* "Safe" code (where the compiler will not let you write code that contains UB).
* "Verified" code (where the compiler will let you write whatever you want, but you also write a machine-verified proof that no UB will actually occur).

But then this is just a matter of definitions - You can set up your build system in such a way that it will refuse to compile unsafe code without a valid proof of soundness. Then you can consider the proof to be part of the source code, and now your unsafe language, plus the theorem proving language, together function as a safe language.

Formally verified microkernels already exist. The sticking point, to my understanding, is the lack (or at least incompleteness) of a verified-or-safe userland.

Undefined Behaviour as usual

Posted Feb 26, 2024 10:02 UTC (Mon) by farnz (subscriber, #17727) [Link] (1 responses)

The other sticking point is the difficulty of formal verification using current techniques. Formally verifying seL4 took about 20 person-years to verify code that took 2 person-years to write.

Undefined Behaviour as usual

Posted Feb 26, 2024 10:12 UTC (Mon) by NYKevin (subscriber, #129325) [Link]

The thing to bear in mind is that, technically, the type checking in a safe language is also a valid proof of safety (or else it would not type check). So every safe Rust program (and every Java program, etc.) is verifiably safe, assuming the type system is sound.*

The question is, is that good enough? Most formal verification wants to prove more than "mere" type safety or soundness, and that tends to be hard because the property you're trying to prove is complex and highly specific to the individual application. But if you just want to prove a lack of UB, that's probably more feasible.

* There are soundness bugs in the current implementation of Rust. Most of them are rather hard to trigger accidentally, but they do exist.