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

51–60 of 135 posts

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

#51

Post by ironman1478 »

stan_rogers wrote: post #49
ironman1478 wrote: post #39

Earlier quoted context omitted.

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.

No. Failed tests can only tell you that you've found a problem; passed tests can't tell you there aren't any problems present. Provably correct code can be proven correct.

Hmm. What if your unit tests are statements about your code? I view them as a way of locking in functionality and saying that the code does or doesn't do things for certain inputs. That's what unit tests are in my mind. I find it strange to view tests as only way a of catching bugs. You just use them to say what your code is/isn't capable of doing.

Using tests as a way of finding problems seems like not a great way of saying code has issues x,y, and z but they are a great of saying something does a, b, c. If you are going through a refactor you might not be implementing a, b or c correctly anymore and if your tests are designed well this will be caught.

If we are only talking about bug catching, you are right there are better tools. But I'll say if somebody says code does something and there are no tests demonstrating that fact, I don't trust it generally unless it's something like a game where it's hard to test certain things.

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

#52

Post by [deleted] »

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.

[deleted]

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

#53

Post by trinovantes »

wikibob wrote: post #43
8note wrote: post #36

Earlier quoted context omitted.

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

Says who?

It's a protected job title in most state/provincial governments

For example, "In Ontario, the titles 'engineer' and 'professional engineer' are restricted by law ... When individuals are found to be using the restricted title 'engineer,' the courts can impose fines, restraining orders and jail time" [1].

It's just hardly reported/enforced in the software industry because most "software engineers" do not work on things that affect public safety or can result in loss of life.

[1] https://www.peo.on.ca/engineering-licensing-body-clarifies-u...

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

#54

Post by toast0 »

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…

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.

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

#55

Post by andrekandre »

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…

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

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

#56

Post by astrange »

bhaak wrote: post #14
sidlls wrote: post #8

Earlier quoted context omitted.

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.

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 regression tests because they're guaranteed to have already found at least one bug.

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

#57

Post by MaxBarraclough »

ntietz wrote: post #18
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…

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.

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.

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

#58

Post by libraryofbabel »

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.

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.

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

#59

Post by garethrowlands »

macintux wrote: post #46
boustrophedon wrote: post #44

Earlier quoted context omitted.

The implication there is that you may have other bugs (i.e. logic bugs, cache invalidation errors, off by one errors) but your program will not crash due to memory issues. It removes a class of errors. It's not saying that it will provide wrong results in cases where it would crash otherwise due to memory errors.

Right. As I realized later, I have a bias: to me, Rust is solving the wrong problem. Crashing is a useful tool when using the right language.

It's not about not crashing. C lacks memory safety, which leads to many bugs, many of which are security vulnerabilities. Memory safe languages such as python or rust just don't have those problems. The vast majority of languages are memory safe but only C is to-the-metal fast. Well, until Rust came along.

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

#60

Post by garethrowlands »

macintux wrote: post #46
boustrophedon wrote: post #44

Earlier quoted context omitted.

The implication there is that you may have other bugs (i.e. logic bugs, cache invalidation errors, off by one errors) but your program will not crash due to memory issues. It removes a class of errors. It's not saying that it will provide wrong results in cases where it would crash otherwise due to memory errors.

Right. As I realized later, I have a bias: to me, Rust is solving the wrong problem. Crashing is a useful tool when using the right language.

What is the right problem? What would you _like_ Rust to be solving?
Post reply on HN