Where are we going from here? Software engineering needs formal methods • Hacker News Board

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

#11

Post by j1elo » Sat, Jul 03, 2021, 9:54 PM UTC

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

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

#12

Post by j1elo » Sat, Jul 03, 2021, 9:57 PM UTC

sidlls wrote: post #8

bhaak wrote: post #7

Earlier quoted context omitted.

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

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?

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

#13

Post by ntietz » Sat, Jul 03, 2021, 9:58 PM UTC

kolinko wrote: post #9

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.

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.

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

#14

Post by bhaak » Sat, Jul 03, 2021, 9:59 PM UTC

sidlls wrote: post #8

bhaak wrote: post #7

Earlier quoted context omitted.

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

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 found with manual testing before they go into production.

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

#15

Post by FpUser » Sat, Jul 03, 2021, 10:00 PM UTC

sidlls wrote: post #8

bhaak wrote: post #7

Earlier quoted context omitted.

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

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.

I once had this fun contract to fix code in one giant application written in PHP. The org of decent size who wrote said code in a first place had code reviews, unit tests and what not.

The end result was that they had to hire outside person to fix what they have produced. I looked through the software and noticed whole bunch of iffy patterns. Ended up writing giant Python script that searched said patterns and fixed it where possible marking with appropriate comments and issued a warning comments where it could not.

Not sure if this is a regular occurrence in companies that write and maintain their internal software as this was the only time I did job like this.

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

#16

Post by ntietz » Sat, Jul 03, 2021, 10:01 PM UTC

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.

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.

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

#17

Post by colordrops » Sat, Jul 03, 2021, 10:02 PM UTC

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…

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.

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

#18

Post by ntietz » Sat, Jul 03, 2021, 10:03 PM UTC

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.

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

#19

Post by api » Sat, Jul 03, 2021, 10:09 PM UTC

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.

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

#20

Post by macintux » Sat, Jul 03, 2021, 10:12 PM UTC

api wrote: post #19

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.

Doing the wrong thing is almost always worse than crashing.