A brief philosophical aside. Tests are almost entirely about seeing into the future. By simply writing down the expected outputs of an operation, that means that we know what they should be ahead of time. We are the so called test oracle. In model-based testing, we instead delegate this prediction to the model: the model is the oracle.
Nice way to look at it!
I’ve been putting off learning prophecy variables; in refinement mappings, are they a way of injecting prescience into an algorithm so it can refine non-machine-closed liveness properties of an abstract spec, or is that something else?
The primary purpose of prophecy variables is to enable showing that a spec implements another one when at least one is nondeterministic. All of the examples where I’ve found them useful are when the implementation is nondeterministic and the abstract spec is deterministic.
The specs in the “Simple Prophecy Variables” section (4.2) of Prophecy Made Simple are a good example. The abstract spec is a process that receives a stream of integers and calculates their cumulative average. The implementation does the same thing, except there’s also an “undo” operation, where an integer can be ignored after being received and the average never gets calculated for it. Since that implementation spec is nondeterministic, you can’t write a refinement mapping because you’ll eventually hit a case where two states in the implementation try to map to a single one in the spec, and they conflict. The prophecy variable solves this by telling you which operation will be taken ahead of time, so you can use that to relate to the correct abstract states. This makes more sense visually, I could send you a diagram if you want.
This undo example is basically the exact same thing as nondeterministic errors, and that’s what made me realize that a prophecy variable would be helpful in testing those. I know way less about machine closure and liveness properties in general. So maybe there are applications there, but in all of the papers I’ve read about prophecy variables this isn’t mentioned.
I’ll definitely give this a read, thanks for sharing.
It seems like testing for refinement has a couple of nice properties for practical application. 1, it’s easier to generate tests if refinement is your correctness statement. 2, testing for refinement is much easier than proving it.
That is an interesting thought. I would love to hear your idea. I do not have much experience to generate tests for refinement. The paper used generic testcases to expose typical bugs in the design.
It can be harder to prove; requires a global invariant. The upside is there is only one property to prove.
For #1 (generating a refinement test), my idea there is model transformation: you write the abstract spec and use the structure of the model to generate a refinement test. Because it’s a test and performance matters, you’ll likely want to generate a test similar to the one in this post, i.e. using refinement mapping / simulation rather than actually checking for behavior sequences.
I’m playing around with that idea in a model transformation language based on metaprogramming. Here’s a simple spec for some CRUD-like behavior. And here’s a “transformation script” which generates the necessary data setup boilerplate for each action. This isn’t a complete example yet, but it’s pretty close to generating the test in this post.
There’s also Cogent, which is a language with a certifying compiler, where each compiler run generates a proof that the generated C code refines the more abstract semantics of the source language.
I initially wanted to make a similar certifying compiler, but since I’m targeting web applications, it’s a lot more difficult to build a general purpose compiler for that (though I am still giving it a go as a long shot). It’s a lot easier to focus on generating only the test suite from a model, and leaving the implementation to still be handwritten.
That is an interesting view point and use of “compiler” to transform test from an High level semantic to the low level semantics.
Am i correct that to begin with the test is generated for a property written in the abstract model?
Well, what I’ve been trying to get across is more like the following:
We write a spec / model in the high-level semantics
We hand-write an implementation
A refinement test is generated from the model that compares model and implementation
It sounds like you might be talking about checking properties about the model. That’s definitely possible, and a workflow I think makes a lot of sense since if refinement holds, then properties about the model are also true of the implementation. But, I haven’t done anything to aid that workflow exactly yet. I’m just focusing on getting to the point where generating a refinement test has good UX.
Testing is much deeply integrated into interactive theorem proving in ACL2s, a variant of ACL2. Theorem proving and falsification help coexist in a tight loop and assist each other.
There has been lot of work on compositional notions of refinement and verification methodology in formal community that is language agnostic . For example, Semantics of a program is defined as a set of traces or computation trees. Compositional verification (abadi and lamport 1993, Kedar namjoshi and Trefler 2000, and many others) then describe sound ways of compositionally verifying the correctness.
And then there are the language-based approaches as described in the paper.
Has there been any effort to reconcile at least the notion of correctness (and better also the proof methods) between the two approaches.
My dirty secret as a computer scientist is that I’m terrible at writing and reading proofs. This interactive tutorial on the Sequent Calculus was the first time that I could do anything useful and it helped me a great deal.
Here’s the thing I always wonder about: is there anything I could actually use this for in daily practice? All the examples are always either trivial or abstract (or both). Have you ever used something like this to solve a nontrivial, but concrete, problem to e.g. simplify a program? Where simple boolean arithmetic, perhaps with a truth table thrown in, didn’t cut it?
So to be honest, I have used Alloy for much of this. More than any theorem prover, the specification capability was most beneficial. At this juncture, anyone would be remiss not to point out Hillel Wayne and his excellent work in this area.
For a gentle introduction to formal reasoning, I would strongly recommend looking at ACL2s and the undergraduate course based on it. It comes with a reasonable eclipse support.
I was a TA for this course few years back and it was interesting to see student with basic programming knowledge and no formal methods background use the tool in a very fruitful way. Of course, for more advanced usage, there has been a multiple decades of work in the industry and academics with ACL2 (theorem proved on which ACL2s is based on).
There is a follow up paper by the authors Layered Concurrent Programs . They develop language constructs to ease specification and establishing refinement proofs of concurrent programs.
One concern about this approach is the trustworthiness of the verification condition generator (VCG). There has been some effort to mechanically verifying the VCG. The complexity of any such approach is directly related to the semantics of the two languages under consideration.
I found this educational and interesting, but I still didn’t find anything to tell me why I need formal methods on top of or in contrast to a testing + static types approach (leaving aside contracts, which I’ve barely touched, and which you mention as one of the three methods for specifying code in the “Getting the Spec” section). You seem to suggest that you can get to 99% correct without formal methods in the “Why Bother?” section…so why would I bother with formal methods? I don’t feel like you answered this in a way I could understand–forgive me if I’m just not getting it.
More specifically, if I’ve already invested a lot of time and energy into learning about type systems and everything they can encode, why wouldn’t I just push ahead with learning more about e.g. dependent types, which seem like they can do a lot of the same, like encoding the proof for a sorting algorithm, similarly to the insertion sort example you gave. Or say we’re concerned with distributed system issues–would we be better served if we could actually encode our message-passing protocol in the type system? Or what about starting from the spec itself to generate programs/proofs–amazing stuff! But do they achieve everything you can achieve with formal methods, with the same amount of effort (acknowledging that some of the stuff I listed above is still more theoretical than practical)? You say there is overlap in PLT and formal methods…where is that overlap, meaningfully speaking? I’d love for you to expand more on your points re: Pony/Rust/Haskell at the end of the “Partial Code Verification” section. Or, let’s assume I’ve bought into the value of spec/design languages as a given…what can they express, or what mechanistic approaches do they provide for verification that I couldn’t get through using a (sufficiently sophisticated) type system? Your description of a model checker sounds a lot like property-based testing, how are these effectively different for my purposes as an industry programmer working on…um, web and mobile apps?
I hope it’s clear that I’m sincerely curious about this, and not trying to cast doubt on the value of formal methods. I also want to be clear that I don’t think static typing is a silver bullet or sufficient on its own, and I recognize that the approaches I’ve suggested above have their own limitations and challenges; I myself have written plenty of Haskell code that type-checks perfectly and is absolutely, horrendously incorrect (I think I’m quite good at this actually). I don’t have the knowledge to state that one is better than the other and I believe it’s more nuanced than that regardless. I guess what I’m trying to glean, fundamentally, is how much energy to expend on learning more about formal methods, and in order to do so I want to know exactly what they can and can’t do in contrast to the approaches I already know, and how hard they are to leverage. I didn’t get that from this piece, and in fact it almost seems like you’re arguing “well, if 99% is good enough then maybe formal methods aren’t for you…” but I suspect that’s not the right takeaway.
Let me just reiterate: this was a very informative and interesting piece, and thank you for writing it. It just left me with more questions!
Thanks for the questions! Lemme see if I can answer a few:
You seem to suggest that you can get to 99% correct without formal methods in the “Why Bother?” section…so why would I bother with formal methods? I don’t feel like you answered this in a way I could understand–forgive me if I’m just not getting it.
Well it’s called “Why don’t people use formal methods?”, not “why should people use formal methods?” :P
More seriously, I wrote this because, as a formal methods expert, I think there are important challenges in the field and serious tradeoffs in practice. Most anti-FM pieces I see, though, miss almost all the nuance, focusing on minor issues and ignoring the major ones. I don’t want to evangelize something I can’t also tear to pieces.
wouldn’t I just push ahead with learning more about e.g. dependent types, which seem like they can do a lot of the same, like encoding the proof for a sorting algorithm, similarly to the insertion sort example you gave.
Dependent types are considered formal methods. Here’s an implementation of insertion sort in Idris, which leverages dependent types to prove the list is sorted.
The challenge with dependent types, though, is the same as the challenge with logics and theorems: specifying them is hard, and verifying them is much harder.
Or say we’re concerned with distributed system issues–would we be better served if we could actually encode our message-passing protocol in the type system?
Message passing protocols are a relatively small part of the challenges of a distributed system. It definitely would help to be able to say we don’t send messages after we close the channel. But what if I want to guarantee that my MapReduce design will always compute the correct answer? Or that my deployment system does not surface different application versions? Or that S3 works right? All of these are pretty easy to do with design specifications, but very hard to do with code verifications.
The difference, I think, is that concurrent types are theoretically effective for simple problems, while design specifications are empirically effective for large problems.
Or what about starting from the spec itself to generate programs/proofs–amazing stuff!
I was lucky enough to see that talk in person: Nadia Polikaporva is one of my heroes and I probably would have attended even if the talk was “birdwatching 101”. I don’t remember whether she talked about it in the talk or in the questions after, though, but she cautioned us that synthesis is nowhere near production ready. I vaguely remember it being something like “definitely not in the next ten years”, at least, and probably a lot longer.
But do they achieve everything you can achieve with formal methods, with the same amount of effort (acknowledging that some of the stuff I listed above is still more theoretical than practical)?
The “more theoretical than practical” part is really important here. In theory, there’s no difference between theory and practice. In practice, there is. Remember, the first formal verification languages came out fifty years ago, and dependent types as a concept are even older. We’ve had a lot ideas on how to make formal verification easier, but so far most of them haven’t panned out.
Your description of a model checker sounds a lot like property-based testing, how are these effectively different for my purposes as an industry programmer working on…um, web and mobile apps?
Model checking tends to work as formal design verification, PBT is usually informal code verification. The advantages of the former are:
Exhaustive coverage
Higher level analysis
Model checkers can check additional properties, such as liveness, things like “all received messages are eventually responded to.”
The downside, of course, is that they can’t check the code itself. There’s not a whole lot of overlap between the PBT and FM worlds, which is a huge shame, because the two have a lot ot learn from each other.
Re web and mobile apps: I got started with FM by applying it to web apps. I gave a talk on it here. It probably saved us about 300k a year purely in business savings, and about half as much again in saved maintenance time.
I didn’t get that from this piece, and in fact it almost seems like you’re arguing “well, if 99% is good enough then maybe formal methods aren’t for you…” but I suspect that’s not the right takeaway.
Haha, well it might be! Most of my essays are super, super pro formal methods. My biases are that in the vast majority of cases, formal design and code specification are incredibly valuable. But in almost all cases, code verification is not worth the expense. However, I also wanted to be clear on why it’s not worth the expense, and how we know when we’ve found cases where it is worth the expense. There’s a lot of careful nuance here and I don’t want to overgeneralize.
Hillel, sorry for my slow response–I just got busy. Thank you very much for your thoughtful reply. It helped me to understand better where I’ve been making the wrong assumptions (I did not realize dependent types were considered as a form of formal methods!) or confusing concepts (I think I’d been conflating code verification and design verification, for one…there are more). I’m going to go back and read your post again, but I’ll just add that this sentence in particular:
The difference, I think, is that concurrent types are theoretically effective for simple problems, while design specifications are empirically effective for large problems.
…helped some things click for me, even thinking more generally than just about session types–it seems like there’s a germ of a statement about the qualities that make static typing distinct from formal methods in terms of where and when and how they are useful. Although, I could be reading too much into it.
I was lucky enough to see that talk in person: Nadia Polikaporva is one of my heroes and I probably would have attended even if the talk was “birdwatching 101”. I don’t remember whether she talked about it in the talk or in the questions after, though, but she cautioned us that synthesis is nowhere near production ready.
Ha, then we were in the same room together, assuming we’re both talking about Strange Loop last year. I loved that talk, it was maybe my favorite talk at Strange Loop leaving aside Frank Pfenning’s talk at PWLConf (one of my other links was to the slides for that talk). I was very impressed with Prof. Polikaporva, both in terms of the vision she presented and in her ability to make a compelling presentation. I have to admit I left the room somewhat quickly at the end because there was such a crowd forming around her, but it sounds like I should have stuck around!
Formal methods has applications beyond “verification”. Several problem,with relative ease, can be modeled in decidable fragments of logic. This coupled with the advancement of efficient decision (and semi decision procedures), gives us a new set of tools for analyses.
Consider for example, efficient code generation in compilers[1,2], and successful synthesize of system architectures for Boeing’s 787 [3].
So formal methods is not just about proving correctness as an afterthought. Rather developments in formal methods can provide value in other aspects of design flow as well.
Nice way to look at it!
I’ve been putting off learning prophecy variables; in refinement mappings, are they a way of injecting prescience into an algorithm so it can refine non-machine-closed liveness properties of an abstract spec, or is that something else?
The primary purpose of prophecy variables is to enable showing that a spec implements another one when at least one is nondeterministic. All of the examples where I’ve found them useful are when the implementation is nondeterministic and the abstract spec is deterministic.
The specs in the “Simple Prophecy Variables” section (4.2) of Prophecy Made Simple are a good example. The abstract spec is a process that receives a stream of integers and calculates their cumulative average. The implementation does the same thing, except there’s also an “undo” operation, where an integer can be ignored after being received and the average never gets calculated for it. Since that implementation spec is nondeterministic, you can’t write a refinement mapping because you’ll eventually hit a case where two states in the implementation try to map to a single one in the spec, and they conflict. The prophecy variable solves this by telling you which operation will be taken ahead of time, so you can use that to relate to the correct abstract states. This makes more sense visually, I could send you a diagram if you want.
This undo example is basically the exact same thing as nondeterministic errors, and that’s what made me realize that a prophecy variable would be helpful in testing those. I know way less about machine closure and liveness properties in general. So maybe there are applications there, but in all of the papers I’ve read about prophecy variables this isn’t mentioned.
Similar idea of testing based on the notion of refinement (I am one of the authors )
https://arxiv.org/pdf/1703.05317.pdf
I’ll definitely give this a read, thanks for sharing.
It seems like testing for refinement has a couple of nice properties for practical application. 1, it’s easier to generate tests if refinement is your correctness statement. 2, testing for refinement is much easier than proving it.
For #1 (generating a refinement test), my idea there is model transformation: you write the abstract spec and use the structure of the model to generate a refinement test. Because it’s a test and performance matters, you’ll likely want to generate a test similar to the one in this post, i.e. using refinement mapping / simulation rather than actually checking for behavior sequences.
I’m playing around with that idea in a model transformation language based on metaprogramming. Here’s a simple spec for some CRUD-like behavior. And here’s a “transformation script” which generates the necessary data setup boilerplate for each action. This isn’t a complete example yet, but it’s pretty close to generating the test in this post.
There’s also Cogent, which is a language with a certifying compiler, where each compiler run generates a proof that the generated C code refines the more abstract semantics of the source language.
I initially wanted to make a similar certifying compiler, but since I’m targeting web applications, it’s a lot more difficult to build a general purpose compiler for that (though I am still giving it a go as a long shot). It’s a lot easier to focus on generating only the test suite from a model, and leaving the implementation to still be handwritten.
That is an interesting view point and use of “compiler” to transform test from an High level semantic to the low level semantics. Am i correct that to begin with the test is generated for a property written in the abstract model?
Well, what I’ve been trying to get across is more like the following:
It sounds like you might be talking about checking properties about the model. That’s definitely possible, and a workflow I think makes a lot of sense since if refinement holds, then properties about the model are also true of the implementation. But, I haven’t done anything to aid that workflow exactly yet. I’m just focusing on getting to the point where generating a refinement test has good UX.
Integrating Testing and Interactive Theorem Proving
https://arxiv.org/abs/1105.4394
Testing is much deeply integrated into interactive theorem proving in ACL2s, a variant of ACL2. Theorem proving and falsification help coexist in a tight loop and assist each other.
Isabelle also has an auto-quickcheck framework that looks for and provides counterexamples in real time: http://people.irisa.fr/Thomas.Genet/ACF/BiblioIsabelle/Advanced/quickcheckForIsabelleRevisited.pdf
It’s really helpful, and surprisingly fast in many cases.
There has been lot of work on compositional notions of refinement and verification methodology in formal community that is language agnostic . For example, Semantics of a program is defined as a set of traces or computation trees. Compositional verification (abadi and lamport 1993, Kedar namjoshi and Trefler 2000, and many others) then describe sound ways of compositionally verifying the correctness.
And then there are the language-based approaches as described in the paper.
Has there been any effort to reconcile at least the notion of correctness (and better also the proof methods) between the two approaches.
My dirty secret as a computer scientist is that I’m terrible at writing and reading proofs. This interactive tutorial on the Sequent Calculus was the first time that I could do anything useful and it helped me a great deal.
Nice, thanks for the link.
Here’s the thing I always wonder about: is there anything I could actually use this for in daily practice? All the examples are always either trivial or abstract (or both). Have you ever used something like this to solve a nontrivial, but concrete, problem to e.g. simplify a program? Where simple boolean arithmetic, perhaps with a truth table thrown in, didn’t cut it?
So to be honest, I have used Alloy for much of this. More than any theorem prover, the specification capability was most beneficial. At this juncture, anyone would be remiss not to point out Hillel Wayne and his excellent work in this area.
For a gentle introduction to formal reasoning, I would strongly recommend looking at ACL2s and the undergraduate course based on it. It comes with a reasonable eclipse support.
I was a TA for this course few years back and it was interesting to see student with basic programming knowledge and no formal methods background use the tool in a very fruitful way. Of course, for more advanced usage, there has been a multiple decades of work in the industry and academics with ACL2 (theorem proved on which ACL2s is based on).
There is a follow up paper by the authors Layered Concurrent Programs . They develop language constructs to ease specification and establishing refinement proofs of concurrent programs.
Also consider Practical Formal Verification of Domain-Specific Language Applications where IVORY ( a restricted version of the C programming language, embedded in Haskell) and DSL based on UML, were translated in ACL2.
One concern about this approach is the trustworthiness of the verification condition generator (VCG). There has been some effort to mechanically verifying the VCG. The complexity of any such approach is directly related to the semantics of the two languages under consideration.
Thanks for this and Layered Concurrent Programs. :)
I found this educational and interesting, but I still didn’t find anything to tell me why I need formal methods on top of or in contrast to a testing + static types approach (leaving aside contracts, which I’ve barely touched, and which you mention as one of the three methods for specifying code in the “Getting the Spec” section). You seem to suggest that you can get to 99% correct without formal methods in the “Why Bother?” section…so why would I bother with formal methods? I don’t feel like you answered this in a way I could understand–forgive me if I’m just not getting it.
More specifically, if I’ve already invested a lot of time and energy into learning about type systems and everything they can encode, why wouldn’t I just push ahead with learning more about e.g. dependent types, which seem like they can do a lot of the same, like encoding the proof for a sorting algorithm, similarly to the insertion sort example you gave. Or say we’re concerned with distributed system issues–would we be better served if we could actually encode our message-passing protocol in the type system? Or what about starting from the spec itself to generate programs/proofs–amazing stuff! But do they achieve everything you can achieve with formal methods, with the same amount of effort (acknowledging that some of the stuff I listed above is still more theoretical than practical)? You say there is overlap in PLT and formal methods…where is that overlap, meaningfully speaking? I’d love for you to expand more on your points re: Pony/Rust/Haskell at the end of the “Partial Code Verification” section. Or, let’s assume I’ve bought into the value of spec/design languages as a given…what can they express, or what mechanistic approaches do they provide for verification that I couldn’t get through using a (sufficiently sophisticated) type system? Your description of a model checker sounds a lot like property-based testing, how are these effectively different for my purposes as an industry programmer working on…um, web and mobile apps?
I hope it’s clear that I’m sincerely curious about this, and not trying to cast doubt on the value of formal methods. I also want to be clear that I don’t think static typing is a silver bullet or sufficient on its own, and I recognize that the approaches I’ve suggested above have their own limitations and challenges; I myself have written plenty of Haskell code that type-checks perfectly and is absolutely, horrendously incorrect (I think I’m quite good at this actually). I don’t have the knowledge to state that one is better than the other and I believe it’s more nuanced than that regardless. I guess what I’m trying to glean, fundamentally, is how much energy to expend on learning more about formal methods, and in order to do so I want to know exactly what they can and can’t do in contrast to the approaches I already know, and how hard they are to leverage. I didn’t get that from this piece, and in fact it almost seems like you’re arguing “well, if 99% is good enough then maybe formal methods aren’t for you…” but I suspect that’s not the right takeaway.
Let me just reiterate: this was a very informative and interesting piece, and thank you for writing it. It just left me with more questions!
Thanks for the questions! Lemme see if I can answer a few:
Well it’s called “Why don’t people use formal methods?”, not “why should people use formal methods?” :P
More seriously, I wrote this because, as a formal methods expert, I think there are important challenges in the field and serious tradeoffs in practice. Most anti-FM pieces I see, though, miss almost all the nuance, focusing on minor issues and ignoring the major ones. I don’t want to evangelize something I can’t also tear to pieces.
Dependent types are considered formal methods. Here’s an implementation of insertion sort in Idris, which leverages dependent types to prove the list is sorted.
The challenge with dependent types, though, is the same as the challenge with logics and theorems: specifying them is hard, and verifying them is much harder.
Message passing protocols are a relatively small part of the challenges of a distributed system. It definitely would help to be able to say we don’t send messages after we close the channel. But what if I want to guarantee that my MapReduce design will always compute the correct answer? Or that my deployment system does not surface different application versions? Or that S3 works right? All of these are pretty easy to do with design specifications, but very hard to do with code verifications.
The difference, I think, is that concurrent types are theoretically effective for simple problems, while design specifications are empirically effective for large problems.
I was lucky enough to see that talk in person: Nadia Polikaporva is one of my heroes and I probably would have attended even if the talk was “birdwatching 101”. I don’t remember whether she talked about it in the talk or in the questions after, though, but she cautioned us that synthesis is nowhere near production ready. I vaguely remember it being something like “definitely not in the next ten years”, at least, and probably a lot longer.
The “more theoretical than practical” part is really important here. In theory, there’s no difference between theory and practice. In practice, there is. Remember, the first formal verification languages came out fifty years ago, and dependent types as a concept are even older. We’ve had a lot ideas on how to make formal verification easier, but so far most of them haven’t panned out.
Model checking tends to work as formal design verification, PBT is usually informal code verification. The advantages of the former are:
The downside, of course, is that they can’t check the code itself. There’s not a whole lot of overlap between the PBT and FM worlds, which is a huge shame, because the two have a lot ot learn from each other.
Re web and mobile apps: I got started with FM by applying it to web apps. I gave a talk on it here. It probably saved us about 300k a year purely in business savings, and about half as much again in saved maintenance time.
Haha, well it might be! Most of my essays are super, super pro formal methods. My biases are that in the vast majority of cases, formal design and code specification are incredibly valuable. But in almost all cases, code verification is not worth the expense. However, I also wanted to be clear on why it’s not worth the expense, and how we know when we’ve found cases where it is worth the expense. There’s a lot of careful nuance here and I don’t want to overgeneralize.
Hillel, sorry for my slow response–I just got busy. Thank you very much for your thoughtful reply. It helped me to understand better where I’ve been making the wrong assumptions (I did not realize dependent types were considered as a form of formal methods!) or confusing concepts (I think I’d been conflating code verification and design verification, for one…there are more). I’m going to go back and read your post again, but I’ll just add that this sentence in particular:
…helped some things click for me, even thinking more generally than just about session types–it seems like there’s a germ of a statement about the qualities that make static typing distinct from formal methods in terms of where and when and how they are useful. Although, I could be reading too much into it.
Ha, then we were in the same room together, assuming we’re both talking about Strange Loop last year. I loved that talk, it was maybe my favorite talk at Strange Loop leaving aside Frank Pfenning’s talk at PWLConf (one of my other links was to the slides for that talk). I was very impressed with Prof. Polikaporva, both in terms of the vision she presented and in her ability to make a compelling presentation. I have to admit I left the room somewhat quickly at the end because there was such a crowd forming around her, but it sounds like I should have stuck around!
“There’s not a whole lot of overlap between the PBT and FM worlds, which is a huge shame, because the two have a lot ot learn from each other.”
There has been some effort in this direction to have testing and theorem proving work together.
Integrating Testing and Interactive Theorem Proving (https://www.ccs.neu.edu/home/pete/pub/acl2-2011.pdf)
Formal methods has applications beyond “verification”. Several problem,with relative ease, can be modeled in decidable fragments of logic. This coupled with the advancement of efficient decision (and semi decision procedures), gives us a new set of tools for analyses.
Consider for example, efficient code generation in compilers[1,2], and successful synthesize of system architectures for Boeing’s 787 [3].
So formal methods is not just about proving correctness as an afterthought. Rather developments in formal methods can provide value in other aspects of design flow as well.
[1]https://github.com/google/souper/
[2] Static Analysis for GPU Program Performance
[3] Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints
This one caught my attention, so I tracked down the paper - a 2018 Thesis and GitHub repository for future reference.
Hi, Thanks for posting. I am the author of this paper. I would appreciate feedbacks/concerns.