ISoLA 2018: Thoughts on Formal Verification and DSLs
As I had mentioned in my previous post, I have spent the last week at the ISoLA conference. Its main focus is on formal methods, but there was a track on modeling as well, which is why I was there.
The fact that there’s a modeling track at a conference on formal methods suggests there is a synergy between the two fields. However, this synergy was only mentioned (or at least hinted at) in a few talks. I think this synergy should be emphasized, and exploited, much more. A while ago we wrote this paper on DSLs and formal methods that describes our work in the area, and demonstrates some of the benefits of using the two together, so this view is not new for me. But there are some new thoughts after ISoLA.
Performance vs. Usability
Several talks expressed the view (and demonstrated evidence) that tools such as SMT solvers or model checkers now scale good enough for use in real-world cases, at least if a “sufficiently clever” encoding of the problem is used. When putting more semantics into the program/model in the first place by using DSL, one can exploit these semantics to generate the “clever encoding”. So that’s clearly a synergy.
However, what all speakers said is that the usability of the tools is not where it needs to be. One aspect is the quality (or lack) of IDE support. An obvious synergy with language engineering is to use language workbenches to build good IDEs with reasonable effort.
But there also the more fundamental problem that writing the specs is tedious: they are too low-level, too mathematical for “normal” programmers and, if used as annotations on program code, involve too much (perceived) duplication. There are several things DSLs can help with.
The Problem with Annotations
First, as the lowest-hanging fruit, one can build an IDE that provides IDE support for both the subject language and the annotations. Today the annotations are often put into comments, with limited IDE support, if at all.
Second, as I said above, by using domain-specific constructs in the first place, many of the annotations can be omitted, reducing duplication. The reason for this is that the purpose of the annotations is often to “recover” aspects of the domain semantics that cannot be expressed with (efficient) program code. By using domain-specific extensions and generators, this can be avoided or automated. Of course this raises the issue of the correctness of the transformation; I will cover this in my next Medium post.
But the “duplication” is also beneficial. A proven way of ensuring the correctness of a program is to write it twice, in different formalisms, and execute it twice, in different ways. So by having the code and the spec, the two act as a crosscheck for each other. If this is collapsed into a “domain-specific program” this benefit goes away and we have to trust the transformation; again, I will look at this in my next post.
Specs are supposedly easier to review than the code (“it is obvious to see that…” is something you hear often if the “formal people” explain what they do); so if the verification finds an error it is supposed to be the implementation code that is wrong, not the spec. While this is sometimes true, especially if the code is optimized, it is far from universal. A spec that really captures the full behavior correctly is often not easy to come up with. I guess one has to rely on testing, to some degree, which kinda defeats the purpose. But even if the spec is hard and it’s not clear where the error is, the argument regarding duplication above still holds! Question is just: isn’t there then maybe a simpler way to achieve this redundancy? For example, write a second generator/interpreter and run both in parallel, at least during testing? This is basically what we did in our medical project.
Again: if you use good domain-specific abstractions and notations for the program (or at least the spec), things get easier to review and understand. Tables come to mind!
Verifiability by Design
There are two other things I want to mention. Typically one designs a language and then “connects” it to a verifier to proof certain aspects of programs written in that language. For example, we are currently working on connecting KernelF to an SMT solver. But it turns out that this is a lot of work. One reason is that the original language has not been designed with verification in mind. Another approach would be to use a language that is already verifiable, e.g., the input languages to the verifiers, and then incrementally extend that language towards the domain. Because you define the semantics of the extension by reduction to the (verifiable) base language, you always retain verifiability. Basically do what mbeddr did for C, but do it for a verifiable language. Dan Ratiu’s FASTEN is an example of this based on NuSMV. I think this is very promising. The connection to DSLs and MPS is obvious.
On the Activity of Formalization
A final point. Several people mentioned in their talks that, while the verification itself was useful, in many cases, much of the benefit came from the process of formalising the problem in the first place. Because this requires you to clearly define things and explore corner cases. Sure, the verifier helps you discover those. But even just carefully writing the spec is a benefit.
This is completely in line with my experience with DSLs. The process of designing the language and then writing example code in it helps a lot in understanding the domain. I would go as far as saying that it’s worth it even if you then never use the language in production. But what this also suggests is this: maybe you can get a significant part of the benefit even without formal methods, just by representing your domain in a well-defined, but not (mathematically) formal language.
