Hacker News Reader

Comment by lisper | Hacker News Reader

> Wasn’t the error actually in an unverified subsystem and isomorphic to an error caught by the model checker in a verified subsystem?

No, it was quite a bit more subtle than that. The problem was that there was no mechanism to enforce the use of the formally verified API, and an application programmer put in a direct call to a system function that bypassed that API.

Source: I was the technical lead on the RAX executive.

View on HN

It sounds more like a cautionary tale against bypassing APIs. What part of this is related to formal verification?

This is why friends don't let friends use unsafePerformIO ... or whatever the equivalent was here :)

I'm still a bit confused about the point though. I feel like an adequate rejoinder would be to enforce formal methods at all the levels? I'm obviously not talking specifics (because I don't know them! ... and you do), but this seems like a failure of process or lack of enforcement of formal methods "all the way down" as it were. I dunno, color me confused...

Which almost reads as a cautionary tale about mechanisms like Dust's `unsafe`. Not necessarily the specifics of the Rust, but the overall idea of having a safe (by whatever means) sunset of operations and and additional unsafe operations, which eases code analysis tremendously. You can't got without unsafe in most embedded systems. But it's good to very explicitly mark in the code wherever the unknown depths of UB lurk if not the most attention is exercised.

While this is true, let's not forget that if there's a problem in the unsafe section, the issue can manifest itself much later in the safe code.. I'm not a Rust programmer but I remember reading about such kind of issue (an alignment error if memory serves).

So sometimes you can build a 'self contained' unsafe part made safe with the right API but not always, which is already a significant improvement over other languages which are unsafe all the time..

Reply on news.ycombinator.com