3 ms·

There is no one definition of 'formal verification'. Sel4's verification required developers to specifically demarcate the behaviour they desire and generally r

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/ 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.

moonchild 6y 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/ 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.

moonchild 6y 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/ 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.