Writing correct lock-free and distributed stateful systems in Rust, with TLA+

It wouldn't surprise me if even Frama-C and SPARK have a "trust me" annotation.

It is unclear to me what requirements you're thinking of when you say "should" or "best to". Given that end-to-end verification is virtually impossible today, any verification method you choose would be incomplete at some level. Exactly which compromises you choose to make depend entirely on the particular correctness requirements of your project and the effort you can afford to spend. There is certainly no one right way to use formal methods, and no one right confidence level a project must achieve.

Also, I don't think it's a good idea to call research projects in formal methods "state-of-the-art". State-of-the-art implies a level of practicality that is often absent even from the most promising research. After some years working with formal methods, it becomes painfully clear that there is a huuuge gap between how well things seem to work in the lab and how they work in real life. That is why formal methods is the only subdiscipline in computer science other than AI that has experienced a research winter, due to unrealized promises and expectations. Formal methods researchers are generally very careful in not building up expectations these days (and the discipline as a whole lowered its goals from those it had in the '70s), but some enthusiasts extrapolate statements they make in an unrealistic way.

As much as I love formal methods, like in machine learning, there is a constant struggle between what people imagine it can do and what it actually can. Everyone using formal methods comes to realize this at some point. Here is what the designers of Spec# had to say:

> [A] conclusion we have drawn from our interaction with developers is that real developers do appreciate contracts... Unfortunately, we have also seen an unreasonable seduction with static checking. When programmers see our demos, they often develop a romantic enthusiasm that does not correspond to verification reality. Post-installation depression can then set in as they encounter difficulties while trying to verify their own programs.

But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. SPARK and friends are subsets if their respective languages, implying that there are features of those languages that, if their use is not restricted, inhibit the production of correctness proofs. Rust already has such a thing, by default, in the form of non-unsafe Rust, and the notion of "unsafe" in the context of Rust and Frama-C is not guaranteed to be the same. So what I'm asking is for you to demonstrate something that these other languages can prove that safe Rust can't.

By the way, you've been in Rust threads enough years now championing safe languages that you really no longer have any excuse for not learning Rust. :P

You don't understand the abstract correctly. It relies on having compilers from diverse sources, unlikely to share the same malicious modification. It does not rely on any of them being trusted.

"It is unclear to me what requirements you're thinking of when you say "should" or "best to"."

The goal of making imperative programs correct with formal verification with optionally other methods. SPARK handles it best right now if we're talking knocking out tons of problems with automated provers.

"Given that end-to-end verification is virtually impossible today, any verification method you choose would be incomplete at some level. "

This is true for most software. That's also fine as even informal verification got us quite far. Partial verification with memory- and concurrency-safe language would be great.

"Also, I don't think it's a good idea to call research projects in formal methods "state-of-the-art". State-of-the-art implies a level of practicality that is often absent even from the most promising research."

Maybe, maybe not. The phrases cutting-edge or state-of-the-art usually mean the most recent capabilities coming out of R&D. Many of them are used in experimental prototypes that aren't realistic or not deployed in production form. You'd be correct for those. The claim is incorrect for things such as SPARK which are designed for real-world use, have commercial-grade tooling, and are in industry use. It's cutting edge and quite practical for whatever programs the notation can handle. Even if not full verification, it can help easily verify absence of common errors that lead to crashes or code injection. IRONSIDES DNS picked it for those benefits.

http://ironsides.martincarlisle.com/

"After some years working with formal methods, it becomes painfully clear that there is a huuuge gap between how well things seem to work in the lab and how they work in real life. That is why formal methods is the only subdiscipline in computer science other than AI that has experienced a research winter, due to unrealized promises and expectations. "

I'm with you on that. It's why I distinguish between two kinds of things I promote: things that are worth trying to see what might happen either for theory or practice; things which should work on solving the problem based on prior work. For formal verification, I usually do recommendations on verifying tiny, critical things very similar to prior successes using the tools from prior successes. For instance, I know the Ocaml compiler can be verified similar to prior work since its individual, critical modules are quite similar in their attributes and size. It might be more or less work but it can be done. I can't tell you if you'll need an expert to fully verify your complex, efficient structure in SPARK. That shit is all over the place in difficulty in ways that continually surprise. I'm pretty sure an amateur w/ some training can use a combo of spec-based checks and partial proofs to raise its assurance, though.

I do like your comparison to AI winter. I saw the early papers, esp in high-assurance security, where they thought it was practically all going to get done in a short time. Reality hit. It became niche. It made a comeback with better tooling and hardware but they're more careful now. I still want your references on global, composable correctness possibly being impossible to verify in large programs to be debated by top minds (including skeptics) in the field. Needs way more focus to help us determine how much future activity would be a waste of time/money.

"When programmers see our demos, they often develop a romantic enthusiasm that does not correspond to verification reality."

The problem is they're bait and switched. It happened to me early on. I'd instead like them to see time/labor/defects-detected measurements for formal and informal development. Then, see what level of expertise was available for each. Also see what level of effort went into learning to verify and/or verifying different kinds of things. There's certainly a gap between expectations and reality that needs to be shown up front. Maybe with heuristics or tips on certain categories of program, component, data structure, attribute (eg pointer-heavy), and so on.