In my opinion, formal methods for software engineering have been heavily advocated for by people and organizations who want to sell books, seminars, and conferences. People who want to act as gatekeepers while extracting money from the system and reframe history in their own terms.
That's not to say formal methods are bad per se, there is just a lot of reason to doubt motives and outcomes behind concerted overarching initiatives.
The notion that software engineering should be grouped under civil engineering is misguided. Part of the reason why we're looking to other fields is to profit from their experience (which is good) but part of it is also because we're desiring a kind of legitimacy we feel is absent. It's a reasonable impulse to a degree, for smart people dedicating their productive years to a discipline. We want to do a good job.
The problem is that we have more in common with architects than we do with civil engineers. There are some goals that can be measured with a boolean outcome: does the code compile, is a certain algorithm provably correct given certain conditions, can a building be built. But it gets murky very very quickly: how well does a thing we create serve its purpose? Does it use resources efficiently? How long will a structure last? What kind of adverse conditions will bring it down? Does the thing make people's lives better and if so by what measure? These are a small hint at the questions where formal methods tend to fall down or even work against us.
So do we need overarching formal methods or do we need to be more scientific about specific objectives and measurement of outcomes that are important to us subjectively?
> In my opinion, formal methods for software engineering have been heavily advocated for by people and organizations who want to sell books, seminars, and conferences. People who want to act as gatekeepers while extracting money from the system and reframe history in their own terms.
Is there really that much of an FM consulting-industrial complex? There's me, Galois, Atelier B, and Adacore, those are the only independent FM groups I can think of off the top of my head. And two of those are tied to specific verification languages.
Most of the FM advocates are academics, which is one reason why there's so much friction between industry and academia wrt FM.
I think it depends on what you are building. For example, if you are building a database that houses user data and user credentials, this is is a very well understood thing that experienced professionals can set up quickly, efficiently, and give you both a lot of security and also enough flexibility to build whatever business you want behind it.
And yet, it seems that most companies and websites that handle user credentials do a poor job at it. So there does seem to be an argument in favor of adding formal methods in certain areas of software design and engineering.
One thing that very much distinguishes the software world from every other type of engineering is the complexity and rate of innovation. In software, I can invent and deploy a thing on the same day and the total R&D cost to my company is almost exactly equal to my salary for that day. Whereas for something like a bridge, the R&D cycle for a new bridge invention could be several months and hundreds of thousands of dollars for a similar idea.
Overall, I think the discussion about putting standards in place for certain common activities (network communications, password databases, encryption standards, and similarly well understood areas) is worth having. Though I also would be concerned that state actors would use such standardization to insert weaponized requirements like backdoors, or that regulation would prevent new innovations from gaining a foothold.
The software industry (SWIND for short) is a mixture of unsafe tooling, high-risk practices, sloppy execution, and total delegation of responsibility. So I agree that the SWIND will never be civil engineering. ^_^
A buyer might accept to buy a product without understanding its fitness for purpose, but the vendor should be selling a product that a) does what it claims, and b) can be run safely and securely.
(a) is the art of software development, which you describe. If the buyer and vendor agree on "robustness", there will be design choices and acceptance testing. But (b) does involve some of (a) if we start to question the shop tools of the vendor.
Given that (b) is fundamentally a problem with bad shop tools (a.k.a. language "foot-guns") and education, a major shift needs to happen in SWIND.
> advocated for by people and organizations who want to sell books, seminars, and conferences.
The publishing business is just one of several economies that live on software. Some of it is good. I think it is beneficial to raise awareness of the need for better shop tools. The ambulance-chasing economy of software security is even bigger than publishing. There are some big shops using bad tools. ^_^
> The software industry (SWIND for short) is a mixture of unsafe tooling, high-risk practices, sloppy execution, and total delegation of responsibility. So I agree that the SWIND will never be civil engineering. ^_^
I interviewed a bunch of civil engineers for a journalism project earlier this year, and my main takeaway was never walk over a bridge. We're not that much worse than other branches of engineering in our tooling and practices.
That's not to say formal methods are bad per se, there is just a lot of reason to doubt motives and outcomes behind concerted overarching initiatives.
The notion that software engineering should be grouped under civil engineering is misguided. Part of the reason why we're looking to other fields is to profit from their experience (which is good) but part of it is also because we're desiring a kind of legitimacy we feel is absent. It's a reasonable impulse to a degree, for smart people dedicating their productive years to a discipline. We want to do a good job.
The problem is that we have more in common with architects than we do with civil engineers. There are some goals that can be measured with a boolean outcome: does the code compile, is a certain algorithm provably correct given certain conditions, can a building be built. But it gets murky very very quickly: how well does a thing we create serve its purpose? Does it use resources efficiently? How long will a structure last? What kind of adverse conditions will bring it down? Does the thing make people's lives better and if so by what measure? These are a small hint at the questions where formal methods tend to fall down or even work against us.
So do we need overarching formal methods or do we need to be more scientific about specific objectives and measurement of outcomes that are important to us subjectively?