That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks.
How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation?
Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?
Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended.
If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.
Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense.
Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.
"You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, "
No need to use Ada, though. Similarly powerful options exist for Java and C. The code-level specification language is JML (Java) or ACSL (C), and there are many verification tools, from SMT solvers, through proof assistant obligations, to concolic or randomized test generation.
Nevertheless, you're never certain doing that, either, as you don't formally tie the code-level specification to the high-level specification. That's OK, though, because end-to-end specification is neither required for most software nor currently possible for anything other than small, relatively simple software.
Right, but this is because SPARK is (intentionally) limited. For example, AFAIK, you can't dynamically allocate memory in SPARK. If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same). Java also has automated verification that does separation logic, and works well with dynamic memory (Facebook's Infer).
Languages that truly admit full automatic verification (and are also limited) -- including rich global correctness properties -- are synchronous languages for safety-critical realtime, like SCADE. BTW, SPARK contracts are not so rich. There are many useful properties that you can't express.
"If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same)."
Java has a different model than SPARK. Especially if you're considering verifying it against the JVM or against assembly. SPARK will probably have an advantage given the papers I've read on JML work. Far as it's overall tooling, I'm aware it has a bunch for proofs and testing as it's one of three I mention to look for in supposedly, high-assurance projects (others being C subsets & Ada/SPARK). Infer is new to me, though, so thanks for mentioning it.
"BTW, SPARK contracts are not so rich. There are many useful properties that you can't express."
Hence, work like E-SPARK that combines Event-B and SPARK. Another I saw uses SPARK, TLA+, and UPAAL for timing analysis on stuff already analyzed at component level. Best to mix and match. DeepSpec with CertiKOS is probably state of the art in that far as popular stuff goes. My Brute Force Assurance concept will do it differently if I implement it where I mix automated analysis and testing tools for code generated in C, Java, and SPARK where each's toolchain catches something the others miss. Semantic mismatches could be a problem but I'm hoping something could come out of it.
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.
"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.
"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.
> The goal of making imperative programs correct with formal verification with optionally other methods.
Yes, but correct at what confidence level, given that the higher the confidence the greater the effort, and 100% is generally impossible?
> SPARK handles it best right now
Again, I don't know what you mean by "best". SPARK is a limited language, and there are other limited languages that are even more amenable to verification than SPARK (e.g. SCADE). There's a whole bunch of tradeoffs, and it's unclear how you rank them, saying that one tool is "best".
> Partial verification with memory- and concurrency-safe language would be great.
Again, you're mixing several concepts here, and it's unclear how you rank them. You can ensure memory and concurrency safety with or without language support, and it's unclear what you mean by "partial verification". For example, you could say that guarantees for memory safety and no race conditions are a good sweet spot.
> The claim is incorrect for things such as SPARK which are designed for real-world use
Right, but JML tools are not behind SPARK, and it's unrealistic to expect people to use SPARK for general-purpose programs, as it is not quite a general-purpose language. Also, have you actually used SPARK on a large project yourself? In formal methods, the greatest advocates of certain tools are very often those who have never used them. When you do, you start seeing their limitations, and understand how no specific tool is a panacea and that no tool is "best" for all or even most purposes.
> It might be more or less work but it can be done.
For a very special kind of "can". seL4 is a 10KLOC C program that has been drastically dumbed down, and still took 20 man years! The people who worked on it told me that they believe it could now be done in 5 years, but even 5 years for an extra-simplified 10KLOC program is well beyond practicality for the vast majority of software.
> 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.
That depends on what you mean by amateur and by how much the assurance is raised. For example, SPARK simply cannot express global correctness conditions, let alone check them. Clearly, when you write a database and want to ensure serializability or no loss of data on failure, those are the most important properties by far. This simply cannot be done with any code-level tools -- like SPARK or JML -- certainly not feasibly.
I haven't tried SPARK myself, but I have tried JML with OpenJML, which is very similar, and I agree with Amazon that TLA+ gives you a bang-for-the-buck that is probably an order of magnitude greater than other approaches. Of course, you can then apply JML to code-level.
> 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.
There is no point to debate something that has been proven, but there's a big difference between what's proven in principle and what happens in practice, going both ways. It is certainly possible that even though correctness provably doesn't compose, it still turns out that for most programs people write, there is an affordable way to verify them. As there is no research -- as far as I know -- that tries to classify what constitutes a "reasonable program", the only way to know is simply to try various methods. To date, we simply have not been able to verify a large program end-to-end, and have not been able to verify small programs affordably. This is a simple fact. It is certainly possible that research will eventually find an approach that works, but it's not like we have a solution for real software today.
"Again, I don't know what you mean by "best". SPARK is a"
The OP is about TLA+ and Rust. Using Rust says they want something imperative, low-level, safe and fast. They also want easier verification. That eliminates all complicated tools (esp proof assistants) plus most of full verification. The parent of my first comment wanted to connect properties proven in TLA+ to the code itself. Maintaining low effort, that narrows it down to Frama-C, Java/JML, and SPARK. If they're a C expert, Frama-C is compelling due to all the other tools that can help them. Java/JML has a similar argument but complex runtime & patent suit-loving vendor (i.e. Oracle). SPARK has high automation, knocks out most of C's problems automatically, has tool support, and a non-malicious vendor. So, solution for this proposal is to try to encode correctness conditions from TLA+ or another analysis in SPARK.
"You can ensure memory and concurrency safety with or without language support, and it's unclear what you mean by "partial verification". For example, you could say that guarantees for memory safety and no race conditions are a good sweet spot."
Full verification is verification of all properties of an algorithm. Partial verification is verifying some of them. You don't really rank the two so much as you prioritize which properties to verify in a partial verification since you lacked time, budget, etc for full verification. Far as memory-safety and race freedom, OP chose Rust which already has that. So, it's a high priority to meet the safety standard OP already desires and has with TLA+ w/ Rust. It's really the OP's preference for easy, specific forms of safety, and efficient imperative language that are dictating my requirements here.
"For a very special kind of "can". seL4 is a 10KLOC C program that has been drastically dumbed down, and still took 20 man years! "
You keep leaving off two things when you mention that. One is that these projects have a habit of reinventing the wheel in tooling using their own languages, runtimes, extensions, new logics, etc. Reuse happens but CompSci likes building new stuff. They usually list around 70% or whatever high number of their effort goes into building new tools/theories. Reusing would drop that down a lot which is where the 5 years comes from. Strictly building on what we have would make that the median or max for a similar project with time coming down further as reusable components are developed. One can see that in ACL2, Isabelle/HOL and Coq ecosystems for projects that actually use what's already there. Or even in CompCert work where new CompSci just keeps adding new components to it to save time/effort.
The other thing is that seL4 targeted C language. That language wasn't designed for verification. By its history, it was barely designed at all starting with BCPL. This was also on shittiest, most-evolution-driven ISA in existence. They also built lots of new tools on top of some of the hardest ones. This thing was set up to be one of the hardest verifications in existence. Proven tools with languages designed to utilize them would reduce the hardness and increase iteration speed. We can see this with Myreen et al's work on CakeML vs CompCert. So much more has happened in less time since they started with a building block (a LISP verified to ASM), built another (a partial SML verified to ASM), and so on to get the big project (decent SML w/ optimizations verified to ASM). Their work was even used in seL4 to verify its assembly. That let it bypass building or needing a certified, optimizing compiler. Likewise, untrusted optimizations + verified, equivalence check let hardware and software verification cheat past a ton of difficulty w/ production cost being sequentially or concurrently running the checker over and over. Lots of potential cheats when designing for easy work w/ lots of reuse. Still hard but not seL4 hard for everything.
"Clearly, when you write a database and want to ensure serializability or no loss of data on failure, those are the most important properties by far. "
Such properties are to be done in another tool then broken down into properties to test on local, code modules. I imagine they'd need at least one specialist for that kind of verification. A database is hard enough that they'd probably be able to hire one. In any case, the OP is using TLA+ to check properties Rust can't. This would be using TLA+ or some other tool to check properties SPARK can't. Similar territory. Also, recall the COGENT work where the key components of an ext2 filesystem was done with half the code in C without painful analysis of mutable state that seL4 had to do. Easier proofs with C code coming out that preserves those properties.
"As there is no research -- as far as I know -- that tries to classify what constitutes a "reasonable program","
There has been under LANGSEC and prior in Abstract, State Machines. They verified them sequentially then their interactions in composition. The thing many keep rediscovering is the model for expressing them has to keep a certain amount of sequential and simple operation. Past as certain point, it becomes impossible to analyze automatically with existing methods. I'm not sure how much work has been done outside the ASM or LANGSEC research on that. We get it incidentally at least during the formal verification efforts: every attempt tells us what can be expressed, proven, etc. Really ad hoc, though.
> Maintaining low effort, that narrows it down to Frama-C, Java/JML, and SPARK.
Not really. Frama-C aside, JML and SPARK simply cannot express those global correctness properties you naturally express in TLA+. Frama-C is really a set of ad-hoc tools.
> So, solution for this proposal is to try to encode correctness conditions from TLA+ or another analysis in SPARK.
But SPARK simply isn't rich enough to do that in general. You're right that if the TLA+ specification is at an abstraction level that's very close to the code, you can try to express some of those properties in SPARK, but I doubt even that is possible. Concurrent algorithms require liveness properties, and I'd be very surprised if SPARK could express them.
There is something interesting you could try, though: You could express global correctness properties in TLA+, and show (in TLA+) that they are preserved if some simple low-level properties are preserved, and then express and verify those in JML/SPARK. This is very interesting, and I'd love to hear about such an experience (or even try it myself), but my gut feeling is that that it would still be too costly. If someone does do that, however, that's something certainly publication-worthy.
> One can see that in ACL2, Isabelle/HOL and Coq ecosystems for projects that actually use what's already there. Or even in CompCert work where new CompSci just keeps adding new components to it to save time/effort.
But I still don't know of a single nontrivial real-world project that has been affordably verified, even with all that reuse.
> The other thing is that seL4 targeted C language. That language wasn't designed for verification...
Again, everything you say is true, but still there are no examples of affordably end-to-end-verified real-world projects.
> I imagine they'd need at least one specialist for that kind of verification.
Not if TLA+ is used. Amazon (and I, too) specify and verify such properties all the time and they (and I) are not verification experts.
> Also, recall the COGENT work where the key components of an ext2 filesystem was done with half the code in C without painful analysis of mutable state that seL4 had to do. Easier proofs with C code coming out that preserves those properties.
I know the person behind Cogent (he'd also worked on seL4), but he points out that the language targets a very narrow domain. Most programs you can think of cannot be written in Cogent.
> Really ad hoc, though.
That pretty much sums up all of formal methods at this stage, especially end-to-end ones. TLA+ is relatively rare in its universality and depth, but it intentionally gives up on end-to-end both because it is currently infeasible (in general) and because 99.99% of software simply doesn't require such strong guarantees.
"There is something interesting you could try, though: You could express global correctness properties in TLA+, and show (in TLA+) that they are preserved if some simple low-level properties are preserved, and then express and verify those in JML/SPARK. This is very interesting, and I'd love to hear about such an experience (or even try it myself), but my gut feeling is that that it would still be too costly. If someone does do that, however, that's something certainly publication-worthy."
That might have been how E-SPARK connected Event-B and SPARK. TLA+ is easier to use than Evdnt-B and often in similar domains. Ill try to remember this option.
https://en.wikipedia.org/wiki/SPARK_(programming_language)
http://www.electronicdesign.com/industrial/rust-and-spark-so...
Here's an example of combining Event-B with SPARK to split overall verification between tools with each handling what they're good at:
https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f37...