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

#41

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

tralarpa wrote: post #32

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

This is some absolutely amazing writing. Good heavens, your line about debating whether a hammer or a saw is the right tool for inserting a screw?? Beautiful!!

Do you blog? If so, I’d love to read more of you. If not, again, this is some seriously good writing. Big, end of a long drunken night “I really love you man, woman or whatever” ups!!!

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

#42

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

fridif wrote: post #34

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

Contrary, formal methods could (in theory!!) give as way to assess correctness of software regardless of programmer qualifications.

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

#43

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

8note wrote: post #36

fridif wrote: 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

Says who?

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

#44

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

macintux wrote: post #26

bhaak wrote: post #23

Earlier quoted context omitted.

You read that wrong. Rust eliminates a complete class of bugs. Memory safety bugs just don't exist. Logic bugs are another class of bugs. Formal methods can help you with those though.

This is what I'm responding to: > It may not do precisely what you want but it will run and not crash. To me, that's a bad thing. I'd rather my software fail entirely than give incorrect results. So what did I read wrong?

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.

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

#45

Post by goodpoint » Sat, Jul 03, 2021, 11:02 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.

There is a ton of memory-safe languages out there.

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

#46

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

boustrophedon wrote: post #44

macintux wrote: post #26

Earlier quoted context omitted.

This is what I'm responding to: > It may not do precisely what you want but it will run and not crash. To me, that's a bad thing. I'd rather my software fail entirely than give incorrect results. So what did I read wrong?

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.

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

#47

Post by codeulike » Sat, Jul 03, 2021, 11:04 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…

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 stage. Or, the users that gave the requirements actually meant something slightly different and that only becomes apparent once the software is infront of them for usertesting.

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

#48

Post by maest » Sat, Jul 03, 2021, 11:05 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…

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

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

#49

Post by stan_rogers » Sat, Jul 03, 2021, 11:06 PM UTC

ironman1478 wrote: post #39

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.

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.

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

#50

Post by boustrophedon » Sat, Jul 03, 2021, 11:08 PM UTC

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.

You can still crash voluntarily via abort! and panic! if that's what you prefer when your program encounters an error.