Live data from Hacker News

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

ntietz.com

71–80 of 135 posts

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

#71
post #48
post #11

Earlier quoted context omitted.

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 would…

> 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 sig…

Everything you can do in software someone could do with a few ASICs. software is several orders of magnitude cheaper, and that is before you account for hhihiwhow eeeasy it is to change.

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

#72
post #11

Earlier quoted context omitted.

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 would…

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…

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

True, but there is no excuse for that anymore. Very little software is really new anymore, so we should have a good handle on requirements by now. (I don't either )

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

#73
post #11

Earlier quoted context omitted.

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 would…

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 :)

Flexibility and Standardization is a tradeoff and how useful each one is depends on the context.

Should you put a project on hold if you only have 1/2 inch nails and the plans ask for 3/4 inch nails? I don't know, are you building a nuclear reactor or a decorative birdhouse?

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

#74
post #14

Earlier quoted context omitted.

Does your opinion only apply to unit testing or to automatic testing in general? I can't imagine the kind of software that wouldn't benefit from automatic testing (unless you would be writing the simplest of CRUD web apps or doing it completely wrong). From personal experience I see both better code design from being forced to make the code testable and less bugs due to writing tests revealing bugs I wouldn't have fo…

> Does your opinion only apply to unit testing or to automatic testing in general? In my experience once people learn about tests, they want to see 1. tests per commit and 2. high code coverage. This leads to unit tests, which don't really test much of anything, and what they do test (the layers under you like the compiler) is by accident. The most useful testing would be integration tests on the side, and then regre…

This, exactly.

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

#75
post #11

Earlier quoted context omitted.

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 would…

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…

Bridges change all the time too!

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

#76
post #36
post #34

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

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

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".

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

#78
post #6
post #4

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.

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?

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

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

#79
> 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.

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

#80

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 spur…

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

Post reply on HN