Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

ntietz.com

Post reply on HN
Print view View original

31–40 of 135 posts

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

#31

Post by nextos »

werpon wrote: 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.

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.

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

#32

Post by tralarpa »

j1elo wrote: post #11
werpon wrote: 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.

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

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

#33

Post by markus_zhang »

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.

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

#35

Post by bobthechef »

bhaak wrote: post #5
rebelos wrote: post #2

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

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.

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.

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

#37

Post by oneplane »

bhaak wrote: post #5
rebelos wrote: post #2

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

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.

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.

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

#39

Post by ironman1478 »

bhaak wrote: post #7
sidlls wrote: post #3

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.

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

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.

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

#40

Post by paiute »

pydry wrote: post #27

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

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