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

#131

Post by hwayne » Mon, Jul 05, 2021, 2:33 AM UTC

heresie-dabord wrote: post #125

hwayne wrote: post #120

Earlier quoted context omitted.

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

The hierarchy of professional diligence, from highest to lowest, would be: * avionics/aeronautics * chemical/electrical/mechanical * civil engineering * automobile industry * movie stunts and pyrotechnics * art installations * software [!] [!] To be honest, this is the exception in this list, because there is no accountability.

Have you ever met any chemical engineers?

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

#132

Post by test_epsilon » Mon, Jul 05, 2021, 1:50 PM UTC

liketochill wrote: post #130

test_epsilon wrote: post #100

Earlier quoted context omitted.

You didn't really address what I wrote though. And I disagree, it does fit the pattern which is what my whole rant was about. You seem to have a romanticized idea of what "real" engineers do as well. A _lot_ of it involves software, a lot of it is prototyping and finding bugs and hacking around them and refining. If you don't like the digital electrical engineering because it's too close to software for you, try mech…

But there is a warranty. I think what a lot of computer programming goes on by people who call themselves software engineers but don’t follow engineering methods and ethics, such as prototyping, and having warranties and liability for the work. I have known some old school engineers who were inspiring in their depth of knowledge, ability to do research and solve new problems, and management of customer and employee r…

So even if we ignore for a minute that software can have warranties... having a warranty? Really? That's what you're going try to say means software development is not an engineering discipline? You could have just accepted my arguments with some grace. You don't expect me to dignify this with a response surely.

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

#133

Post by liketochill » Mon, Jul 05, 2021, 4:04 PM UTC

test_epsilon wrote: post #132

liketochill wrote: post #130

Earlier quoted context omitted.

But there is a warranty. I think what a lot of computer programming goes on by people who call themselves software engineers but don’t follow engineering methods and ethics, such as prototyping, and having warranties and liability for the work. I have known some old school engineers who were inspiring in their depth of knowledge, ability to do research and solve new problems, and management of customer and employee r…

So even if we ignore for a minute that software can have warranties... having a warranty? Really? That's what you're going try to say means software development is not an engineering discipline? You could have just accepted my arguments with some grace. You don't expect me to dignify this with a response surely.

As an end user of software I don’t have SLAs or warranties, just EULAs that guarantee nothing and the ground constantly shifting underneath me with updates that take away features or turn me in to a subscription revenue stream as some functionality is unnecessarily moved to the cloud.

I am sure there is software created by an engineering process by software engineers, but it is probably less visible to me in my day to day computing. The effort you detailed that is required to make sure a chip works is a good one.

And I agree electrical and computer engineering are disciplines.

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

#134

Post by pron » Wed, Jul 07, 2021, 8:19 AM UTC

hintymad wrote: post #24

It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will. Besides, TLA+ is not panacea in formal methods. It’s a specification language, which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concepts, such as spur…

> TLA+ is not panacea

Of course it isn't, but neither is testing, and we all still do it. The only question that matters is, does it have a good ROI or not? TLA+ does in a wide range of problems.

> which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concept

That all sounds imposing, but TLA+ users usually don't "master" any of those, and reaching a level of high utility takes far less time than achieving the same with any programming language. Writing useful specifications that can save real money takes something like 3-4 full days of a workshop or 2-4 weeks of after-hours self study. Learning how to read specifications well enough to implement them takes much less (a few hours to one day), and doesn't require any temporal logic at all.

It's certainly possible that it's still not for the majority of engineers, but most teams will have at least one person who can do it, and that might be enough.

> such as spurious counterexamples

???

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

#135

Post by pron » Wed, Jul 07, 2021, 8:25 AM UTC

zozbot234 wrote: post #65

hintymad wrote: post #24

It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will. Besides, TLA+ is not panacea in formal methods. It’s a specification language, which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concepts, such as spur…

The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system. You're making up a simplified "toy" model of your software architecture and verifying claims about your toy model, that may or may not apply to your actual code. This is sometimes justifiable when the software architecture is the most interesting thing you're dealing with, but that's not a very common case. Most programs are designed in…

> The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system.

That's a huge benefit, rather than a pitfall at all. End-to-end verification of real-world systems ranges between the impractical through the infeasible to the downright impossible. The biggest software ever verified end-to-end at the same depth as TLA+ was 5x smaller than jQuery, required extraordinary simplification, and still took world experts years. People have found serious bugs in software ten times the size of the largest program even verified end-to-end within days of starting to learn TLA+.

The question is not whether TLA+ can achieve a feat nothing else can, anyway, but whether it has a good ROI.