[nickpsecurity]

Thanks for insightful reply. The difficulties make more sense now. Far as why at the end, the guarantees formal verification give you can far exceed basic, memory safety for common usage. That's why for many verification projects.

[cwzwarich]

To clarify: I was rhetorically asking why one would bother with the complexity of completely verifying a program in Rust rather than C, not why one would want full verification rather than memory safety.

[nickpsecurity]

(a) The program had to be written in Rust as part of a whole application or for seemless interoperability

(b) You wanted to avoid problems of C. Opposed to it in general with Rust an option.

(c) Your hardware architecture easily supported Rust's safe subset but not C's model. Examples include Burroughs, Ten15, Java CPU, and SAFE (crash-safe.org) CPU's. Edit to say may as I'm not a Rust programmer. C being very unconstrained breaks most of these models.

(d) Others have proven precedents but this is speculative: doing a split between formal verification and type system for safety. A number of projects have done this. A simplifying example is that you model check or verify an abstract design that you code a Rust equivalent to. The semantics helps with the abstraction that knocks out A, B, and C classes of problems. The proven type system of Rust (or SPARK or whatever) is leveraged for X, Y, and Z problem classes. Each method is applied where it's strong.

These are best a quick brainstorm can do at this hour for me. :)