3 ms·

"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 verif

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

pron 9y ago
> 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.

pron 9y ago

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