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

111–120 of 135 posts

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

#111

Post by Taek »

rhizome wrote: post #108
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.

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.

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.

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

#112

Post by heresie-dabord »

ud_0 wrote: post #105

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…

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

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

#113

Post by TheOtherHobbes »

taeric wrote: post #83
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.

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.

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.

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

#114

Post by TheOtherHobbes »

MaxBarraclough wrote: post #57
ntietz wrote: post #18

Earlier quoted context omitted.

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

It's astounding that core security infrastructure isn't formally designed and certified, and isn't available as standardised - certified - drop-in elements.

A top decile PhD thesis is not a high bar in engineering. It's how most disciplines evolve. "Not invented here" is not a credible explanation for why CS feels a need to be different.

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

#115

Post by deregulateMed »

notriddle wrote: post #93
deregulateMed wrote: post #69

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?" Sub…

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

That article proved nothing.

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

#116

Post by sidlls »

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

Do you know of any formal study that talks about this?

It's pretty easy to find various papers/studies about TDD, unit testing, and the like by searching online but I would not call any of them scientifically or empirically rigorous. Given the lack of any objective or agreeable standards regarding what "code quality" means, these papers can draw conclusions to support any view.

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

#117

Post by Akronymus »

tsimionescu wrote: post #96
SkyMarshal wrote: post #95

Earlier quoted context omitted.

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

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.

Good defaults are one of the most important, yet overlooked parts of programming languages IMO.

For example, no nullability or mutability by default is one of the main reasons why I like f#.

https://onor.io/2012/03/27/why-the-defaults-matter/

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

#119

Post by SkyMarshal »

tsimionescu wrote: post #96
SkyMarshal wrote: post #95

Earlier quoted context omitted.

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

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.

>Rather, better defaults in web and SQL frameworks, even in a dynamic language, would get you most of the way there.

We’ve had 20+ years of building websites, and either we have sane defaults by now but they’re not enough, or we still don’t have sane defaults in our web frameworks.

Either way, that this problem persists given the damage it’s enabling, suggests we haven’t addressed the root cause yet. Web development is still a tarpit, which strong type systems can mitigate in unique ways.

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

#120

Post by hwayne »

heresie-dabord wrote: post #112
ud_0 wrote: post #105

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…

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…

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

Post reply on HN