Have you looked at Ada/SPARK? Since SPARK is an Ada subset and both can exist in the same project, you write SPARK when you need verification and Ada if there’s areas where you don’t need it or don’t need it yet. There’s even proved libraries written which are in the Ada/SPARK package manager, Alire.
Where I found myself disagreeing was with the initial premise … “The job of a software engineer is not to produce code, but to solve problems”.
While that is the job for some, a large proportion have the job of modeling a system in code, and the two are different. A problem that culminates in an algorithm is certainly a candidate for a specification that can be formalized. Is that the case for a complex problem domain under consideration that is a model of a system - real or imagined?
That new innovative but complex international payroll system that needs to be built, faces an entirely different set of issues. How are functional requirements and domain constraints determined and modeled in code? How are non-functional requirements determined and met within project/product and organizational constraints?
Perhaps at question is the simplistic viewpoint that all software development is just the transformation of data. I disagree with such a contention. While inherently accurate, it’s similar to saying that the materials used to construct furniture is just atoms.
How to model complex systems in code in any formal and predictable way remains out of reach, and is why calls for applying the terms “formal methods” and “engineering” to software development is inapplicable for many?
Even cutting-edge domain problems still use a lot of basic infrastructural code to run. Does the international payroll system use a rules engine? Is it running batch jobs as background tasks, or triggering anything reactively? How are you distinguishing employee benefits from benefit classes? All of those are places where formal methods help.
More fundamentally, it’s possible for stated requirements to not cover a situation, or give you contradictory results on how to handle a weird edge case. Shouldn’t it be possible to find those out before you’ve written all the code?
Sure there are parts where formal methods might be applied. But I contend they simply are not “the” answer to what is fundamentally a different problem. As is the case all too often in our profession, I see the original author as generalizing all software development towards a particular “silver bullet”.
Yeah, I definitely don’t think formal methods are “the” answer. I think there are more people who could use them that don’t than people who don’t need them but think they do, but it’s ludicrous to collapse all of software engineering down to a specific technique.
I didn’t mean to (and I don’t think I did) generalize that all development has to lean toward formal methods, nor is it a silver bullet. But I think software engineering as a field needs it, and there are a lot of bits of critical code that need it, and as a trend I think we’re pushing toward making it easier to use and using it in more places.
As an aside and by way of apology, I was updating my answer as you replied. It my weird (?) way of writing something and then changing it for the first few minutes after first submitting it. HN handles this well by giving 10 minutes in which one can change a reply before it is published. Not sure if Lobsters does the same.
There’s also the classic tools Isabelle and Coq. Isabelle was used to prove correctness of seL4, and Coq was used to prove the four-color theorem and to verify CompCert.. Both of these can also produce executable code, which is nice since there is less chance of divergence of code and model.
Ada was already mentioned in a different comment, but it falls in the same category as the above.
Then there’s the thing that drives the autonomous Paris metro, written in Event-B.
Then there’s also Lean, although it more in the direction of mathematical work if I am not mistaken.
I bet there’s a lot of other tools out there that I’ve forgotten, but these are also worth a look if you are interested in formal verification IMO.
So, where does that take us? Well, we want to do engineering to solve problems. I think that means, practically speaking, we need to focus on the specification and verification steps
Respectfully, I disagree. After thrashing around in this area for many years, I’m convinced that the code doesn’t matter, although coding is the thing most of us love doing.
Tests are the things that are most important, whether implied or explicit. Most tests, of course, are sub rosa; they seem too trivial for anybody to ever write down. (Until they fail, of course)
What we need to work on are truly modular and composable tests, something that scales out. my formal methods should revolve around those. I understand that this can be construed as saying the same thing, but there are several subtle differences between the two concepts.
I think, at least directionally, we agree: the focus is on showing that your code does what you want it to do, and the code itself doesn’t really matter.
Have you looked at Ada/SPARK? Since SPARK is an Ada subset and both can exist in the same project, you write SPARK when you need verification and Ada if there’s areas where you don’t need it or don’t need it yet. There’s even proved libraries written which are in the Ada/SPARK package manager, Alire.
It’s on my list of things to look into! TLA+ is earlier on my list but Ada and SPARK are near the top, too.
Where I found myself disagreeing was with the initial premise … “The job of a software engineer is not to produce code, but to solve problems”.
While that is the job for some, a large proportion have the job of modeling a system in code, and the two are different. A problem that culminates in an algorithm is certainly a candidate for a specification that can be formalized. Is that the case for a complex problem domain under consideration that is a model of a system - real or imagined?
That new innovative but complex international payroll system that needs to be built, faces an entirely different set of issues. How are functional requirements and domain constraints determined and modeled in code? How are non-functional requirements determined and met within project/product and organizational constraints?
Perhaps at question is the simplistic viewpoint that all software development is just the transformation of data. I disagree with such a contention. While inherently accurate, it’s similar to saying that the materials used to construct furniture is just atoms.
How to model complex systems in code in any formal and predictable way remains out of reach, and is why calls for applying the terms “formal methods” and “engineering” to software development is inapplicable for many?
Even cutting-edge domain problems still use a lot of basic infrastructural code to run. Does the international payroll system use a rules engine? Is it running batch jobs as background tasks, or triggering anything reactively? How are you distinguishing employee benefits from benefit classes? All of those are places where formal methods help.
More fundamentally, it’s possible for stated requirements to not cover a situation, or give you contradictory results on how to handle a weird edge case. Shouldn’t it be possible to find those out before you’ve written all the code?
Sure there are parts where formal methods might be applied. But I contend they simply are not “the” answer to what is fundamentally a different problem. As is the case all too often in our profession, I see the original author as generalizing all software development towards a particular “silver bullet”.
Yeah, I definitely don’t think formal methods are “the” answer. I think there are more people who could use them that don’t than people who don’t need them but think they do, but it’s ludicrous to collapse all of software engineering down to a specific technique.
I didn’t mean to (and I don’t think I did) generalize that all development has to lean toward formal methods, nor is it a silver bullet. But I think software engineering as a field needs it, and there are a lot of bits of critical code that need it, and as a trend I think we’re pushing toward making it easier to use and using it in more places.
I do agree. Formal methods can certainly be of benefit.
My suggestion is to better define where, for what types of software and under what circumstances.
That is what would really benefit the developer community in my opinion.
As an aside and by way of apology, I was updating my answer as you replied. It my weird (?) way of writing something and then changing it for the first few minutes after first submitting it. HN handles this well by giving 10 minutes in which one can change a reply before it is published. Not sure if Lobsters does the same.
There’s also the classic tools Isabelle and Coq. Isabelle was used to prove correctness of seL4, and Coq was used to prove the four-color theorem and to verify CompCert.. Both of these can also produce executable code, which is nice since there is less chance of divergence of code and model.
Ada was already mentioned in a different comment, but it falls in the same category as the above.
Then there’s the thing that drives the autonomous Paris metro, written in Event-B.
Then there’s also Lean, although it more in the direction of mathematical work if I am not mistaken.
I bet there’s a lot of other tools out there that I’ve forgotten, but these are also worth a look if you are interested in formal verification IMO.
Also worth looking at F*, which is used in Project Everest (a formally verified TLS stack used in Firefox and Azure).
Perfect place for me to shill Let’s Prove Leftpad
Respectfully, I disagree. After thrashing around in this area for many years, I’m convinced that the code doesn’t matter, although coding is the thing most of us love doing.
Tests are the things that are most important, whether implied or explicit. Most tests, of course, are sub rosa; they seem too trivial for anybody to ever write down. (Until they fail, of course)
What we need to work on are truly modular and composable tests, something that scales out. my formal methods should revolve around those. I understand that this can be construed as saying the same thing, but there are several subtle differences between the two concepts.
I think, at least directionally, we agree: the focus is on showing that your code does what you want it to do, and the code itself doesn’t really matter.