Strumenta 
We interviewed Rutger Van Beusekom the CTO at Verum, a company based in The Netherlands. We talk about a domain specific language that they have been developed at Verum for supporting formal verification of code, in particular for embedded systems.
Federico Tomassetti
So, hello Rutger, it’s very nice to have you here today. How are you today?
Rutger Van Beusekom
I’m doing well, suffering from serious cold, having traveled to San Francisco. 9 hours time difference and sleeping not too well, but beyond that, I’m doing great. Nice to meet you. And thank you for giving us the opportunity to talk about our passions.
Federico Tomassetti
Okay, so we can appreciate a lot that you took the effort after just coming back from San Francisco to take this interview. And yeah, we’ll just say that you are the CTO at Verum, a company based in The Netherlands. Today, we are here to discuss a domain specific language that you have been developed at Verum for supporting formal verification of code, in particular for embedded systems. So I hope I get the overview, right. But of course, we will dive into more details. As we proceed in the interview. I think it makes sense to start with telling us a little bit about your company Verum.
Rutger Van Beusekom
They’re actually founded in 2004. So we’ve been around for a while, and the original founders have left in the meantime; and I’ve taken over in the role of CTO. Officially since 2019, but effectively already since 2014. Yeah we’ve been serving with an original product, which was called ASD at the beginning and later on the rebooted the company in creative Dezyne. We’ve been serving companies like ASML, Phillips and Thermo Fisher, which all exist in the Eindhoven region in the Netherlands. So or focus has been quite close to home.And now we’re starting to expand our horizon.
Federico Tomassetti
Well, quite a list of impressive clients. So it’s not easy to find clients at that level. Okay, and today, in particular, we want to discuss about Dezyne, your domain specific language. So why did you create it in the first place?
Rutger Van Beusekom
I grew up actually, within Philips, that’s where I started, and Phillips, was doing, was adopting object orientation at that time. And I spent less time doing object orientation, which is inherently imperative. Doing that in a concurrent environment, is basically a recipe for disaster. It is just too complicated to get right. Especially on embedded systems, where you interact with the physical world, and having some form of correctness is paramount. And I was introduced to the concept of model checking at my time at Phillips by the original founder of Verum. And having seen that was a eureka moment for me. I have to do something with this. So that’s the mission. Bringing formal methods, model checking, to the masses, basically.
Federico Tomassetti
Yes. And can you tell us about the ideal user that you have in mind for design?
Rutger Van Beusekom
Preferably, in the future, and that’s not where we are today. Anyone using a language like C or C++, or C#, Java, Python, doing a serious amount of development, where either asynchronicity or concurrency plays a role, whether it’s in a cyber physical system or not, but with a high level of complexity, they should benefit from fully automated verification. So that’s the group we are aiming for. As far as I’m concerned, basically every programmer. But we’re trying to lift to the level of abstraction, in order to capture requirements at the formal level, such that you can prove that throughout the entire state space of your software system, and even the system of systems. This sounds very ambitious, we’re not quite there yet. That’s the end goal.
Federico Tomassetti
Good. So. Okay, so it’s clear that you’re targeting developers. And so is the main advantage for them, basically, they get formal verification for free by using the language or is something else?
Rutger Van Beusekom
I want to say yes, but verification is not a free lunch, you still have to express what you want to prove, formally. So if you’re not willing to do that work, like doing test driven development, you’ll have to write the tests, and you have to do that intelligently. Otherwise, they will not help you. The same holds for describing the essential properties that you need to prove automatically. But that’s, that’s the unique selling point, yes. The scope of what we’re trying to do is larger, effectively, we’re trying to augment our limited human mental capacity, using the power of the computer. There are, of course, automation is one big thing, so we’re doing code generation, we’re doing simulation, we’re doing verification. That automates a lot of the work that we, as humans can do with our brain, but we’re not just not that good at it, to do it systematically and completely and correctly. It’s better to have the computer do that for us. So effectively, we’re trying to figure out a new way of software engineering, which connects to the existing ways of software engineering, but raising the bar.
Federico Tomassetti
So, you right, correct me when I say that formal verification comes for free, because it doesn’t come for free, or if I understand correctly, require an extra effort. And so to your users, or the people that you discuss with value, formal verification enough to accept this extra effort. So do, do they see the value this?
Rutger Van Beusekom
We have quite, we’ve been able to quite naturally embed certain implicit requirements into our language.I will briefly explain what the nature of the language is. So I talked about object orientation in concurrent environment. Our language supports component based development, which I look at as a subset of object orientation, a stricter subject. In object orientation, nothing limits you, you can make it as complicated as you want, in our approach components, are very strict. A component is completely encapsulated behavior, being unaware of what the state or the implementation details behind its formal interfaces are. So design requires you to model any interaction with a formal interface. And an interface is just like an API, it lists the functions you could call out or receive, with data or not, with return values or not. But we also describe the protocol of that API explicitly. And then, in our model checking, we prove that you’ve got an effective protocol contract that implementations on either side of the interface maintain that contract. And that’s a very natural way for most software engineers with at least some object oriented background to describe their software. On top of that, we have user definable properties that can be expressed as boolean predicates across many interfaces, or all across the local components state variables. Language is inherently imperative. But also declarative, somehow, I won’t go into detail. If you want to know more, have a look dezyne.org, we can find all the information you want.
Federico Tomassetti
Can what were the main challenges in designing such a language? I suppose it’s the first language you design, or not?
Rutger Van Beusekom
When I joined Verum, there was a prototype of the concept of the original CTO, which is called ASD, or Analytical Software Design, I think it was called. And effectively, it was inspired by the clean room method by Harlan Mills, I believe, which was a tabular notation effectively of a state machine. And it already had the concept of something like components and interfaces. But because it was a table, it was not actually a language, as such. So in Dezyne, we added the textual notation. And there has been many, many challenges, from a business point of view. From a management point of view, or funding point of view, technology, and people point of view. I don’t know. I guess your listeners would be mostly interested in the technical side of things.
Federico Tomassetti
All the aspects are interesting, because, you know, if you’ve write a great language from the technical point of view, but then you don’t get support from people, then there is no point. So
Rutger Van Beusekom
Exactly. That’s still our biggest challenge, stepping out into the world and, well finding recognition. That’s why we’re still actively developing the language, we don’t believe ourselves that it’s quite finished yet. Cooperating with our current customers is a great help there. Yeah, if you’ve got more specific questions, for challenges, I had more than happy to answer those. Otherwise, I’ll just continue ranting
Federico Tomassetti
then I would be interested in editor support because one aspect that sometimes people building language underestimate is the difficulty of building an editor. So I wanted to ask, what efforts have you done in this area or
Rutger Van Beusekom
We’ve had many experiments, and enough failures, which is a successful experiment, of course, finding out that something doesn’t work. And on the editor support we definitely had a few of them. So our original product was a completely purpose built Excel like editor, which I personally found horrible, but some people really liked. But that was the old product, when we started designing a textual language, it was the intent to be able to use any editor to write the language but of course, modern programmers expect significant editor support. And initially, we selected Eclipse as the launching editor to be in, and we effectively developed using Xtend, I think it’s called, the language support. But in the end, it resulted in having, I believe, four or five separate parsers for the same language. So I really wanted to unify all of those parts into a single implementation they could serve all the different uses of parsing. So, finally, we settled on. We use scheme to do most of our developments. Dezyne is actually developed, written in scheme. In scheme, we use Guile as our scheme implementation. It has a PEG, a Parser Expression grammar library, which we extended, which is now being used in our LSP, Langiage Server Protocol plugin, we use it in our compiler for all the different use cases that that our language offers, so we’re able to make a single parser to rule them all. But that has been quite a challenge.
Federico Tomassetti
And it’s it’s an experience that I can relate to because I also started my adventure in this area by using Xtext that I think at the time was great than then probably Eclipse didn’t evolve, as well as we were hoping, maybe. But about evolutions, I think it will be interesting to hear about your plans for language, if you plans more of more work on the technical side or on the promotion side or any other direction, which you may want to work.
Rutger Van Beusekom
So as CTO, my two primary goals or assignments are to, to push for, for more recognition in the outside world, build a community. But in doing that, of course, address or close the gap to what people actually need and expect from such a language. And for the foreseeable future, we identified that we need to make data a first class citizen in Dezyne. So we do support data, but if you take a single 32 bit integer, the state space of that integer is already vast. From my head, it’s more than 4 billion numbers. And in combining a few entities would blow up the state space during verification. So doing this effectively, is what we need to achieve. Because that’s one of the extensions we’re thinking of. And a long standing feature that we want is system wide functional verification. So I talked about those user defined properties. We’ve come up with the language extension to express those properties, just boolean predicates. But we need to lift that to the composition of our components to be able to do that performantly, at the system level. So we believe that that is what the community is lacking for large scale pickup of Dezyne.
Federico Tomassetti
And maybe this is connected to the promotion side. But I also saw that you had a couple of publications on your work. So I wanted to ask you about your speed and see if about your experience in general with scientific publications.
Rutger Van Beusekom
I’d like to spend more time publishing about Dezyne, because I think that’s an essential platform to get the message across. And it’s also a way to have at least academic community validates what we’re doing, or invalidates such that we can actually address those things. Yeah, I think there’s three papers out there now on Dezyne. Actually hoped to start promotion work at some point and use that as a driving force to produce more of those papers. I think that the last paper was written by Michele, I forget his last name, which I contributed to. So yeah, it would be great if the scientific community wants to research on the basis of what we’re doing? Because we are very much an R&D organization that we can use more help. Publishing is is one of the ways to do that.
Federico Tomassetti
And that you’re lucky to be based in the Netherlands because I think there are several research group doing a lot of work at Delft or Amsterdam in this area. So nice place for being based. And did you find any resistance from developers in adopting domain specific language, because sometimes developers, you know, consider themselves a C++ developer, and you know, it is really part of their identity. So everything else is not their job.
Rutger Van Beusekom
Yeah, not acceptable. That’s an inherent fact, we haven’t figured out a true solution for that. Our approach to this is to have. Dezyne is actually intended as a coordinative language. So about 90% of the software has more or less been written, and we focus on the 10%, which is missing as a society. So we have to be able to deal with the 90%, which is already written. So people should not have to be forced to rewrite that all of that code into a new language. So we’re trying to make Dezyne more like a coordinative language, we’ve, we’ve added model based testing for existing implementations in the hope to bridge the gap for those, for instance, C++ lovers not to have to say goodbye to the code they’re still attached to. And of course, from a monetary point of view, leveraging existing code, which works is essential. But fundamentally, if someone is really in love with a specific language, and they don’t see the benefit of what Dezyne offers, I can only say more power to you. And I expect at some point, you’ll find that it’s it’s a lot of work in conventional languages to be truly productive, and to achieve a level of correctness, which I think society will push to raise the bar on, in the foreseeable future.
Federico Tomassetti
Not sure if I understand exactly to mine, but do you mean that I can have components written in other languages? And right, maybe the combination of these components in Dezyne, or did I misunderstood
Rutger Van Beusekom
Yeah Dezyne is intended to be a hybrid meta language effectively. It principle, you can develop a new code in Dezyne because we generate C++ or C or Java or Python, at request. So if you’re doing greenfield development, all you need is Dezyne. But no one is doing greenfield development, it’s usually brownfield development. So in order to add automated verification to a brownfield, that requires adding specification for what is already there, and proving that, that specification is consistent with those implementations. And we figured out a way to do that using model based testing. And when we have those specifications, we can build the new code using Dezyne on top of that, and know that it’s consistent and correct using model checking. That’s the hybrid approach. So the targets will always, the target code will always be C++ or C, or whatever a user chooses. But they will do their, their orchestration and their verification at the model level an with a push of a button generate the missing bits.
Federico Tomassetti
Makes sense. And so I think, in this interview, we explain the value of Dezyne and so I hope that at this point, people will be interested in learning more about the language so can you give us any pointer for learning more?
Rutger Van Beusekom
Yeah, we have two websites. Free Software, free as in free speech of freedom, not as gratis is dezyne.org, this is where we publish open-source or open-core for Dezyne, were are actually a NON-GNU project and hope to be a full blown GNU project in the future. And we’ve got the commercial websites verum.com where you can get your commercial support. On the only dezyne.org website, we publish the language reference manual, we’ve got tutorials, you can find the source code. And on the commercial site, you can find a binary version and get in contact with our sales.
Federico Tomassetti
So we will make sure to add all the links in the transcript. And so my final question is, what do you plan to work on next?
Rutger Van Beusekom
I think priority one is community building, and secondary, extending the expressiveness of the language and the corresponding tooling. I think we’ve got about five feature branches still up in the air that needs to become part of our release train. So I think in the last 12 months, we have fundamentally extended the language we we’ve added the concept of collateral blocking we’ve added a defer keyword we’ve added the concept of constraining interfaces and shared interface state. So these are all fundamental changes to the language making it more expressive. And we’ll continue to do that in the future. I talked about the system wide functional verification, I think that has the main attention on either side which we will integrate making data as a first class citizen into. Yeah I think that is it for now!
Federico Tomassetti
Enought to keep you busy for a while. Okay, so I think it’s time for me to thank you again for giving this interview and for creating these domain specific language. I think it can be an inspiration for authors to learn from your effort on the technical level and community building level on your experience building also editor support. So I think this has been very valuable and thank you
Rutger Van Beusekom
Thank you very much. I hope it will inspire some someone out there.
Federico Tomassetti
right, so Good
Rutger Van Beusekom
Bye bye
