undefined | Better HN

0 pointsmoonchild5y ago0 comments

> The zen of Rust is not to eliminate unsafe code. That would require a compiler so ludicrously sophisticated that it would be borderline magical

I'm not sure what you mean by ‘borderline magical’. There are formal verification tools for e.g. c and a subset of ada. The sel4 microkernel has been completely formally verified; i.e. it has no unsafe code.

0 comments

2 comments · 1 top-level

zesterer5y ago· 1 in thread

There is no one definition of 'formal verification'. Sel4's verification required developers to specifically demarcate the behaviour they desire and generally requires the use of abstractions with very predictable safe semantics. In addition, Sel4 is less than 9k lines of code.

That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code. That's not the goal of Rust and I doubt that it would be a particularly useful one for 99% of developers anyway. The goal of Rust's safety promise is that the verification and review of an entire codebase (as would be the case in C) shrinks down to just a very small corner of that codebase (that which is demarcated as 'unsafe').

In practice, I think that unsafe uses are substantially rarer than that even. Veloren (https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand.

moonchildOP5y ago

> Sel4 is less than 9k lines of code

By my count, it's approximately 86k loc.

> That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code

Even a language like ATS (which is ‘general-purpose’) can verify a substantial majority of code which would need to be marked ‘unsafe’ under rust. (It also proves a number of other interesting and desirable features, like bounding recursion.)

> I doubt that [complete formal verification, as a goal] would be a particularly useful one for 99% of developers anyway

Why? I find that a pretty attractive proposition.

Safety isn't an end to itself; it's means that enables a broader desire to produce more reliable, correct software. One of the great things that rust (and, to a lesser extent, typescript) have done is to bring more expressive, powerful type systems into vogue. Ones that can more effectively model real-world systems and verify program behaviour. Why choose to stop, arbitrarily, with however much power rust's type system happens to have at the moment?

> Veloren (https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand

Veloren is a video game and arguably has no excuse for having any unsafe code. Redox, which is probably a better case study, uses the keyword 8k times.

j / k navigate · click thread line to collapse