Where are we going from here? Software engineering needs formal methods

https://ntietz.com/tech-blog/future-of-software-engineering-is-formal-methods/

by ntietz • 5 years ago

139 131 5 years ago

rebelos• 5 years ago

Whether or not formal methods can be applied is almost entirely an economic decision since that kind of rigor drives up cost. Makes sense in certain high value systems when the organization wrapped around them has the resources or the level of risk associated with a less rigorous approach is too high (e.g. at NASA).

What the author seems to miss completely is that there are many systems developed using typical methodologies that generate billions in revenue. What this tells you is that ideas like TLA+ are effectively superfluous in a wide variety of software contexts.

bhaak6• 5 years ago

It's not easy to quantify but you can't just dismiss formal methods because we don't know how much development and maintenance overhead they would eliminate.

How much revenue something generates is a poor metric. Otherwise, we all would probably be programming in PHP.

bobthechef• 5 years ago

I don't think the OP dismisses formal methods, only the idea that they have pervasive utility that outweighs costs in most scenarios, at least for certain kinds of formal methods.

But we can't forget the range of formal methods either. Type systems technically qualify, as the article notes, even if they are lightweight, and they're not new. Given the pervasiveness of Java, we're already making widespread use of at least that formal method and have been for a long time.

How much revenue something generates is a poor metric. Otherwise, we all would probably be programming in PHP.

The OP wasn't arguing that revenue is driving or should drive language selection, only that the revenue shows that the lack of formal methods does not seems to prevent companies from making enormous sums of money.

you can't just dismiss formal methods because we don't know how much development and maintenance overhead they would eliminate.

That by itself is not much of a positive argument for their use. And do you know how much maintenance overhead they would introduce? In either case, it might be useful to compare how a switch between similar languages (e.g. JS and Typescript) affected code quality (in terms of the number of bug reports filed, for example) and feature delivery time. Maybe there's a point where the trade off makes sense. In which case, languages that support a gradual adoption of formal methods might begin to look attractive.

oneplane• 5 years ago

The programming language itself has very little to do with the revenue something generates.

Revenue isn't generated by technical details, those are just the implementation of a product that itself is just an implementation of the goals of the business.

The reason people are and aren't programming in PHP is just plain and simple: taste. Maybe ff 10 developers in a team want to use PHP they can just do that, as long as at the end of the line the product delivers. If 3/10 want to use PHP, and 7/10 want to use C# then no, it will not likely run on PHP. And if as a developer you prefer certain features or tools over others, you are likely to select the technologies that suit that.

None of the technical details had anything to do with the value that was created.

If your requirements say that 100 people per minute need to be able to find, basket and purchase product on a website, and those requirements are met, does it really matter if the codebase is a combination of AppleScript and an ActiveX control? (I know, that technically doesn't exist, not the point)

Now, if those requirements also include scaling needs, long-term support needs, knowledge sharing, consultancy options, then you might not select those technologies.

ntietz3• 5 years ago

I mean, it depends on criticality. If something is critical, pushing further along the formal methods spectrum makes sense (see also: why AWS has done a lot with TLA+). Sure, we probably won’t verify all of Instagram, but super critical portions of the platform underlying it are likely worth it and would save money in the long run by reducing outages, bugs, etc.

MaxBarraclough2• 5 years ago

I'm fond of formal methods, but I'll offer the usual counter-example:

Formal methods struggle to scale up to real-world problems. There is no formally verified TCP/IP stack. There is no formally verified TLS or SSH implementation. That's despite how immensely useful and reusable such implementations could be (that is to say, high demand, and yet no supply).

As I understand it we're not even close to being able to develop a formally verified TLS implementation, but if we were, it would likely take the form of an internationally acclaimed PhD thesis, akin to CompCert. It still wouldn't mean formal methods are cheap and easy.

andrekandre• 5 years ago

also, they dont mean bunk if business side of the equation isnt behind them... following formal methods means that business also follows formal business methods (which would reduce sudden changes and mistaken product designs etc).

too many times "dev" is treated like a roving circus that can just change their routine on a dime with little consequences...

sidlls4• 5 years ago

There are plenty of shops that apply rigorous, formal methods to software design. Military contractors providing software for mission critical systems do this (or used to). Some will cut corners, but they are supposed to follow the methods and procedures the contracts specify.

It isn’t common in private industry because it’s typically deemed unimportant.

bhaak6• 5 years ago

You aren't paid either to write unit tests in the private industry.

You are paid to write working code.

sidlls4• 5 years ago

Depends on where you work. The cult of unit testing is pervasive in the Bay Area, at least. It doesn’t result in noticeably better software.

icedchai• 5 years ago

You'd be surprised. Often, the tests are more work than the "working code" itself. At companies that have a test heavy focus, I'd say roughly 50% or 60% of the effort is spent on tests (this includes future work to maintaining tests as they are affected by other areas of the code, etc.) You may not be able to get your PR approved without enough tests.

ironman14782• 5 years ago

How do you know it's working if it doesn't have unit tests that exercise edge cases? Or even basic functionality? Also, good unit testing can allow you to reduce the time it takes to write software by giving you an isolated environment to run your code.

Unit tests are a tool to get you to working code.

ntietz3• 5 years ago

There’s a spectrum of formal methods and with the push toward static types in Python coming directly out of industry I would argue that industry is definitely deeming it important in some degree; the question is to what degree. Right now a lot of the time it’s only worth it for the most critical systems (S3, for example, but not my side project webapp) but if tooling improved, it would be worth it for more cases.

werpon• 5 years ago

Formal methods may work for civil engineering where the usual workflow is gathering requirements, developing a detailed project and building the thing, with the implicit understanding that any little change will mean recalculating costs and deadlines.

When your customer decides to pivot the fintech app you were developing into a cryptocurrency investment tool, it makes no sense.

bhaak6• 5 years ago

How much help your unit tests if your customer pivots from their original idea?

Is that a reason not to write unit tests in the first place?

hwayne7• 5 years ago

Generally unit testing is faster than formal verification, so you're out less work if requirements change.

j1elo2• 5 years ago

In Civil Engineering it would seem crazy that someone changes their mind and decides that the Tower they had requested, obtained designs for, budgeted tens or hundreds of people's work, and planned for, now suddenly must be a Bridge. They themselves would discard the idea due to how absurdly expensive would be to just basically start from scratch. All that money and resources would be basically wasted.

Maybe it wouldn't be a bad thing that the same thing happens, to a lesser extent, in Software Engineering. Say bye to stupid last minute changes caused by the fact that they are not perceived as expensive, and all the bad incentives it creates in the people writing that software.

colordrops• 5 years ago

It would be a bad thing though. The fact that software is changed with so little effort is a feature and a positive aspect. The only thing that should factor into whether a more rigorous approach should be taken is the use case.

tralarpa• 5 years ago

Software engineering is still very far from engineering. It's a young field and everything is still very experimental. Its practitioners are still debating whether a hammer or a saw is the best tool for inserting a screw, and whether to insert the head first or the tip first. Don't forget that the art of building bridges has a head start of several thousand years :)

codeulike• 5 years ago

Say bye to stupid last minute changes ...

Bridges stay the same, software changes all the time and _needs_ to change all the time because the business (or whatever) domain that the software is in is also constantly changing. The reason the 'waterfall' method of "gather requirements, design, build, test" fails so often is that the requirements gathered at the start are often out of date by the time you get to the test stage. Or, the users that gave the requirements actually meant something slightly different and that only becomes apparent once the software is infront of them for usertesting.

maest• 5 years ago

stupid last minute changes

Those are a feature of Software Engineering, as opposed to Civil Engineering.

If there was a cheap way to turn Towers into Bridges (and the cost of failure was comparable to that of an app having an outage), our infrastructure would look a lot different.

I know quickly changing requirements are a pain for those who have to do the implementation, but, commercially, that flexibility has significant value.

toast0• 5 years ago

Building construction is full of last minute changes too, it's just that the scope is usually more limited. But a lot of that also boils down to the cost to make changes.

You better get the foundation of your 100 story tower right, because it's a big, costly pain to fix it later. When update costs and consequences of errors are similarly high in software, you see real effort spent on getting it right before shipping.

When costs to update are low and costs from error are low, less effort is spent on getting it right first.

Personally, I've rarely seen a specification in my career, let alone anything rigorous enough to write a formal specification from. And, even if there were a rigorous specification, everything is subject to redesign at any moment. Not a whole lot of value in formal methods in that kind of environment. You don't tend to get a structural engineer to certify your plans for an overnight camp in a two-person tent.

nextos• 5 years ago

That's a bit extreme. In cases where things move quite quickly, we should still be able to provide some formal guarantees. There's a whole spectrum of formal methods ranging from formal proofs to rich type systems and design by contract.

I have personally had a lot of success with some techniques, and I'm quite hopeful ideas such as those in Liquid Haskell will eventually become mainstream.

taeric2• 5 years ago

I'm pretty sure there has to be some irony involved with this take coming the week of a civil engineered building collapsing in Miami.

Our industry is not unique here. And many formal methods are hidden by the tools of the trade.

TheOtherHobbes2• 5 years ago

The building collapsed because it was poorly maintained and there was serious structural damage - which could easily have been avoided.

This was noted three years ago by a civil engineering inspection, but the building's owners/managers did nothing about it.

rhizome• 5 years ago

Formal methods come from a need for form, repeatability. There is nothing in software development that comes close to the process and considerations that go into choosing to build with M30 concrete, or use #5 rebar for that matter.

Taek2• 5 years ago

Sure there is! The most obvious example to me would be a server-side database for storing user credentials. It's a very common problem, it's well understood by the experts in the industry, and also most everyone makes the wrong choices anyway.

There are plenty of places inside of software that are pure-innovation and can't use a formal process to design and implement, but there are also plenty of places where a corporation just wants a website that does customer loyalty, and you often don't need any innovation at all.

kolinko• 5 years ago

There is a lot of formal method usage in smart contracts. Maker DAO for example did a full formal verification of their stuff, and there is a lot of talk within the security community about it.

ntietz3• 5 years ago

Yes! The blockchain community is doing a lot of cool stuff here and it’s definitely an area where it’s worth it even with less than ideal tools.

api3• 5 years ago

The proper place for these is compilers, linters, fuzzers, unit tests, etc.

Rust does a pretty damn good job of preventing memory and threading errors for example. If it compiles and there is no unsafe it will run. It may not do precisely what you want but it will run and not crash.

macintux6• 5 years ago

Doing the wrong thing is almost always worse than crashing.

bhaak6• 5 years ago

You read that wrong. Rust eliminates a complete class of bugs. Memory safety bugs just don't exist.

Logic bugs are another class of bugs. Formal methods can help you with those though.

goodpoint• 5 years ago

There is a ton of memory-safe languages out there.

totemandtoken• 5 years ago

I wrote a (dummy) paper for a class about automatically generating a formal specification based on a given program using a GAN. I don't really know how feasible it would be, but I feel like that would circumvent some of the issues being brought up in the comments about how difficult it is for organizations to use formal methods in their workflows.

jeffreyrogers• 5 years ago

Code is already a formal specification of sorts. I'm sure more rigor will lead to fewer errors, it also will increase development time, which is a poor tradeoff in many domains. Plus, a source of many bugs is that the specification is wrong, which will remain true even if rigor is increased.

Edit: Of course there is low hanging fruit that can be incorporated into languages. I write a lot fewer bugs in C++ than I do in C and a lot fewer in Swift than I do in C++.

hintymad• 5 years ago

It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will.

Besides, TLA+ is not panacea in formal methods. It’s a specification language, which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concepts, such as spurious counterexamples. And remember that essential complexity is in specifying a system? Now try to specify something as simple as quicksort. Let’s just say specifying a system with mathematical logic is beyond 99.99% of software engineers. Not that people are incapable, but I doubt people have enough incentive to swallow the cost. For one, how much does it cost to debug a spec? Don’t believe me, do try out the book by Hehner: http://www.cs.utoronto.ca/~hehner/FMSD/, or introductory books like this: https://www.amazon.com/Verification-Reactive-Systems-Algorit..., and you’ll get the idea. And yes, I thoroughly studied the mentioned books cover to cover and still think they are not for the majority of software engineers.

lostcolony• 5 years ago

Yep. Anyone who tries to do that in a competitive space will have their lunch eaten by people who slap something together and get it in front of customers.

zozbot2343• 5 years ago

The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system. You're making up a simplified "toy" model of your software architecture and verifying claims about your toy model, that may or may not apply to your actual code. This is sometimes justifiable when the software architecture is the most interesting thing you're dealing with, but that's not a very common case. Most programs are designed in relatively simple ways, and would benefit more from an end-to-end system that establishes valuable properties (even comparatively trivial ones like type and memory safety, or simple pre- and post-conditions) about the actual code one will be executing.

pron2• 5 years ago

The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system.

That's a huge benefit, rather than a pitfall at all. End-to-end verification of real-world systems ranges between the impractical through the infeasible to the downright impossible. The biggest software ever verified end-to-end at the same depth as TLA+ was 5x smaller than jQuery, required extraordinary simplification, and still took world experts years. People have found serious bugs in software ten times the size of the largest program even verified end-to-end within days of starting to learn TLA+.

The question is not whether TLA+ can achieve a feat nothing else can, anyway, but whether it has a good ROI.

hwayne7• 5 years ago

It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will.

I've seen people successfully use formal methods on CRUD apps! The trick is to use more lightweight stuff that gets you some benefit without taking as much time. For example, modeling out the problem domain elements and seeing if there's any pathological cases you need to worry about. This is a particularly good use case for Alloy, since it can make visualizations.

SkyMarshal2• 5 years ago

but I’m not sure a CRUD app will.

Considering most corporate websites are CRUD apps, and they keep getting pwned via some bug or vulnerability and millions of private user information stolen and pawned off in the black market, I don't think that's an assumption we can make anymore.

That said, full-on formal methods may still be overkill. A web framework built in a language with a strong type system and input sanitation via type-checking and similar safeguards may suffice.

But that's closer to formal methods than most of the web dev industry is accustomed to.

tsimionescu• 5 years ago

I'm not sure type safety is the right key here. Rather, better defaults in web and SQL frameworks, even in a dynamic language, would get you most of the way there. You can even use dynamic types to mandate that input is sanitized - a crash is much louder than SQL injection or XSS.

hwayne7• 5 years ago

Most of the recent egregious hacks I can think of were compromised by things like out-of-date software, poor access control, stuff on the configuration level. Static analysis might help here, but I don't think formal methods is the lowest-hanging fruit.

tluyben2• 5 years ago

Not that people are incapable

I think that is quite an overestimation of what most people in the industry can do.

pron2• 5 years ago

TLA+ is not panacea

Of course it isn't, but neither is testing, and we all still do it. The only question that matters is, does it have a good ROI or not? TLA+ does in a wide range of problems.

which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concept

That all sounds imposing, but TLA+ users usually don't "master" any of those, and reaching a level of high utility takes far less time than achieving the same with any programming language. Writing useful specifications that can save real money takes something like 3-4 full days of a workshop or 2-4 weeks of after-hours self study. Learning how to read specifications well enough to implement them takes much less (a few hours to one day), and doesn't require any temporal logic at all.

It's certainly possible that it's still not for the majority of engineers, but most teams will have at least one person who can do it, and that might be enough.

such as spurious counterexamples

???

pydry• 5 years ago

Where the risk of building the thing wrong is outweighed by the risk of building the wrong thing then formal methods make no sense.

andrewnicolalde• 5 years ago

Brilliantly put.

paiute• 5 years ago

people forget that we tried this and it didn't really work out that well. gang of four is only mildly useful.

libraryofbabel• 5 years ago

This is the essence of it.

Formal methods could be useful when requirements are clear, can be strictly defined, aren't going to change suddenly, and the stakes of building it wrong are very high. Avionics. Medical devices. Cars. Some kinds of embedded systems. Core parts of OS Kernels, databases, network stacks, cryptography libraries, etc.

Most software in the world is not like this. It exists to support businesses trying to make a buck in a changing world, either from consumers or from other businesses. Requirements are messy, shift frequently, and agreeing on what they are at all is more than half the battle. Nobody really knows the minutiae of quite how the whole product works but it doesn't really matter. Money is still coming in. The risk to those businesses of even rather bad bugs is generally low. A few customers have a bad day because they see a 500 error in their browser when they're trying to order food, or they can't summon their ride-share for 5 minutes. The issues are fixed and life goes on. The perfection of formal methods is the enemy of good, and would be a net negative return on investment, much as programmers who (understandably) love perfection and clarity and rigor might want it to be otherwise.

solarmist2• 5 years ago

Not yet, but I think we’re getting to the point where software will fractionalize and those pieces will formalize.

TCP/IP stack, crypto libs, message busses, networking libraries are all prime candidates for this kind of formalization.

Right now we’re just waiting on the first mass incident where a component/service is recognized by a government as essential and should be regulated then you’ll quickly see those structures/organizations form around that area.

AlotOfReading• 5 years ago

We all make use of those components though, regardless of how CRUD the application is. We'd all benefit from them being validated. The fact that "fully validated" versions of those components don't exist is simultaneously an indication of how difficult the problem is and how little our industry truly cares about product reliability and quality. These issues are not rare or even particularly uncommon in the wild.

I imagine the pursuit of formal methods in software that doesn't strictly require it would go a long way to fixing other systemic issues like tech debt, security, and performance.

creata• 5 years ago

The issues are fixed and life goes on.

Some bugs can't be fixed: once you've leaked millions of people's personal information, you can't really take it back. The "stakes of building it wrong" are very high in most software, because businesses are all too willing to hoover up all your info.

The risk to those businesses of even rather bad bugs is generally low.

That is unfortunately true, but hopefully we'll eventually manage to hold businesses accountable for their screwups.

allyourhorses• 5 years ago

(1990)

effie3• 5 years ago

So true.

austincheney• 5 years ago

Software isn’t a special unique snowflake as some developers, who have never worked in other fields, will tell you. Software certainly seems unique though when you have no other professional employment experience to compare it to.

The primary problem with missing formal methods is supplemental guidance bolted on artificially in search of a problem producing some canned solution. The reason for that people tend to focus on their personal needs instead of business needs. For example many developers will suggest an approach of personal familiarity even if it costs more, performs poorly, and lowers product quality. Furthermore many developers tend to focus on composition and tools first as opposed to saving composition for the final step and using either no tools or a more correct tool for the job.

Formal methods on the other hand provide guidance for a planning process that articulates the work to be performed opposed to how that work should be done.

markus_zhang• 5 years ago

Comparing to real engineering, I really don't think we can even get close in regarding to project management and expectation handling.

Plus actually real projects frequently go over their budget (by a huge margin), go over their planned time, or go totally wrong.

fridif• 5 years ago

No it does not. Please do not turn software engineering into yet another needlessly licensed profession, it has already been tried.

8note• 5 years ago

Software development*

If you want to call yourself an engineer; the licensing is essential

wikibob• 5 years ago

Says who?

MaxBarraclough2• 5 years ago

Depends on jurisdiction. In the UK anyone can call themselves a software engineer.

effie3• 5 years ago

Everyone knows that software engineer is not an "engineer in the traditional sense". There is no substantial chance of confusing HR or manager hiring for software development when you say to them "I'm software engineer".

m_j_g• 5 years ago

Contrary, formal methods could (in theory!!) give as way to assess correctness of software regardless of programmer qualifications.

zozbot2343• 5 years ago

Relevant blogpost series from hillelwayne: The Crossover Project - Are We Really Engineers? https://www.hillelwayne.com/tags/crossover-project/

deregulateMed2• 5 years ago

Programmers need to come to terms with their jobs being Art and Science rather than Science.

Unless you are keeping track of transistors, you are not doing science/engineering.

Sure we gladly accept the title SWE because it pays well, but in physical world, engineering has a significantly higher qualification for truth.

"Should we write this in x or y? Should we save this as an array or directly in the database?"

Subjective, and impossible to come up with a single, undebatable correct answer.

As opposed to, "What metal should we choose for this wire harness?" With cost and quality metrics, there's only 1 correct answer.

Making a clear cut distinction between engineering and programming would do literal wonders for programming. Anything deemed SWE should be objectively correct. Anything else would be free to be scrutinized by Art, Tradition, Science, and Authority.

notriddle• 5 years ago

https://www.hillelwayne.com/post/crossover-project/are-we-re...

deregulateMed2• 5 years ago

That article proved nothing.

effie3• 5 years ago

But as a goal, that's really what you want: we want to solve the problem by saying "this is the solution" and then poof the solution appears!

Actually, that is very often not the case. Many SW projects start with an idea of what the software should do, but there is no easy way to describe it in full detail. Writing down the complete specification right from the start would be very hard and prone to wasted work.

For example, say you want to write a messaging system. You could try to imagine the whole thing and describe it in some formal language, but this will most often produce huge pile of ideas that weren't tested and are not part of desired solution in the end. It's too much "building in the head".

Instead, we should prototype. We write the simplest possible thing that roughly does what we want, and then add and remove features as convenient/needed and improve various characteristics.

We handle corner cases as they appear, sometimes learn that something new has to be studied / understood first, and some parts that have been written have to be rewritten and then we do so.

Writing the spec for the result may be done in the end, after the software is done and works and the ideas are proven to work.

solarmist2• 5 years ago

I think the way software will evolve into a more traditional engineering role will be in layers of abstraction starting closest to the hardware. Which will become certified services/systems to build more loosely on top of or using as components.

We’re starting to see this with commoditization/formalization of platforms. OS, storage, cloud, infrastructure, e-commerce are getting to the point where they’re pretty well explored. In another 20 years it’ll be so specialized and optimized that you’d need a Ph.D to make meaningful improvements in those areas.

So people won’t feel the need to try and recreate it themselves except for learning and as that process continues we’ll see those things formalize best practices which would eventually turn into engineering standards, etc…

You’ll have licensed and bonded engineers building low level highly formalized systems/services which meet certain guarantees. Similar to how I imagine civil engineering works.

Then for the rest of the industry you’ll have what we currently have which is like home construction where almost anything goes, but there are pieces that need to be validated by actual engineers or licensed professionals similar to how electricians and plumbers are licensed.

cratermoon• 5 years ago

Funny, I was just re-reading this today and thinking about how the industry has played out in the twenty years since. http://www.mcs.vuw.ac.nz/comp/Publications/CS-TR-02-9.abs.ht...

madrox• 5 years ago

I’ve once thought this way, but over the years I’ve come to decide that such formalization will never outpace frameworks. Frameworks are easier to grok and scale better than rigorous education.

hyperpallium2• 5 years ago

These days, coding is the quickest way to find out what's needed. That is: implementation precedes requirements.

This is the real reason software is eating the world. Incumbents lose because aren't able to reorganize themselves around a software core, and so can't try things.

Formal methods are intrinsically satisfying, as are all quests for perfection and truth.

pw262• 5 years ago

For business applications, formal methods are really limited to core algorithms.

The real problem is that data entry and validation should be a solved problem. Sadly this is not the case. Try using .Net WPF or React and your only recourse is to Stack Overflow. These frameworks are over complicated and are full of weird edge cases that make everyday programming tedious and error prone.

Lets get our house in order before we break out the temporal logic.

valenterry• 5 years ago

Is there even a good definition of "engineering" somewhere?

The one from Wikipedia for example is not really great imho, as it can be interpreted to be applicable to almost every job.

sakoht• 5 years ago

"Wouldn't it just be grand if we could write a spec for some piece of code, then let the machines do the rest?"

This is quite possible, if you write the "spec" in a programming language: i.e. write a test case. The problem is that people imagine a formal proof in, for example, English, being simpler or easier to think about than in, say, Python or C. In general this is not true. In general, moment you expect your "spec" (code) to be sufficiently precise for a machine to act upon it, the simplest way to describe it is a programming language.

And if you can invent a better way to describe it, and it is unambiguous enough for a machine to act on it, you've invented a new programming language.

cryptos• 5 years ago

I think a sweet spot is "specification by example" also called behavior driven development (BDD). You take a more or less standardized, but human readable language to write down the specification and implement test adapters for it.

A typical tool for this approach would be Cucumber: https://cucumber.io/

cloogshicer• 5 years ago

Having done BDD at work, I can only say it's not the right approach.

The "human-readableness" of the test cases produced with BDD is debatable - at least at our company only technical people familiar with the code could understand the spec.

At the same time BDD was very cumbersome to do, while not really providing us any benefits.

ud_0• 5 years ago

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?

Taek2• 5 years ago

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.

heresie-dabord2• 5 years ago

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. ^_^

hwayne7• 5 years ago

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.

hwayne7• 5 years ago

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.

pjmlp• 5 years ago

Very unwelcome opinion around here.

We could start by stop calling software engineering to 6 months coding bootcamps, letting it for actual 5 years experience being taught correct engineering practices and respective skill assessment.

Then we can start talking about adopting what is still missing from real engineering practices into the field.

Ah, and in the process make companies liable for skipping quality control when everything goes wrong.

skneko• 5 years ago

I am a research intern working in a group studying and developing formal methods. The tech we are working with has served to verify planes, trains and has been used in NASA. AMA if anyone here is curious about how the world around FM works.

jalcazar• 5 years ago

Program verification is an expensive activity. Navigating the cost-benefit trade-off of program verification is ultimately a business decision. https://t.co/IUCLtDLROC

olivierduval• 5 years ago

Actually, what could really helpful would be a "simple" precond-postcond-invariant calculator...

The principle is quite simple: for every method you write, the "calculator" tells you what "outside" variable are modified. Obviously it seems quite simple with FP... but not so simple with object/imperative language as soon as you start to call other procedures or subsystems or syscall!

Of course, it could be nice that this "calculator" works inline (while you write your code) and not afterwards (when the program is compiled). It should be "smart enough" for example to tell you that your code is calling an INSERT on a database in a sub-sub-sub procedure of your code or that it is effectively calling some file writing somewhere in the called path

Where are we going from here? Software engineering needs formal methods

Related Stories