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.