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

#121

Post by hwayne » Sun, Jul 04, 2021, 4:03 PM UTC

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…

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

Is there really that much of an FM consulting-industrial complex? There's me, Galois, Atelier B, and Adacore, those are the only independent FM groups I can think of off the top of my head. And two of those are tied to specific verification languages.

Most of the FM advocates are academics, which is one reason why there's so much friction between industry and academia wrt FM.

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

#122

Post by hwayne » Sun, Jul 04, 2021, 4:06 PM UTC

SkyMarshal wrote: post #95

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…

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

Most of the recent egregious hacks I can think of were compromised by things like out-of-date software, poor access control, stuff on the configuration level. Static analysis might help here, but I don't think formal methods is the lowest-hanging fruit.

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

#123

Post by api » Sun, Jul 04, 2021, 4:51 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 like security vulnerabilities? I don’t think we are talking about the same thing at all. It’s perfectly easy to make Rust “crash” or log errors when it does the wrong thing, and to write unit tests for it.

Memory errors and threading bugs are never ever something you want.

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

#124

Post by taeric » Sun, Jul 04, 2021, 6:27 PM UTC

TheOtherHobbes wrote: post #113

taeric wrote: post #83

Earlier quoted context omitted.

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.

This doesn't really take away from the point. The life cycle of most software projects is tiny compared to the life cycle of most buildings. And in most all failures, the warnings were clear way in advance.

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

#125

Post by heresie-dabord » Sun, Jul 04, 2021, 7:27 PM UTC

hwayne wrote: post #120

heresie-dabord wrote: post #112

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

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.

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

#126

Post by kinjba11 » Sun, Jul 04, 2021, 7:46 PM UTC

hwayne wrote: post #75

codeulike wrote: post #47

Earlier quoted context omitted.

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…

Bridges change all the time too!

What do you mean by 'bridges change all the time too'? Some of the oldest bridges in the world were built nearly 2000 years ago. That's zero change besides basic upkeep.

What is the oldest unchanging software project you can think of? Typical software projects have a constant accrual of features. Some of the older projects like the Linux kernel are more like a mansion that keeps getting more rooms while others are demolished. Not exactly something that happens to a bridge.

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

#127

Post by olivierduval » Sun, Jul 04, 2021, 8:02 PM UTC

Actually, what could really helpful would be a "simple" precond-postcond-invariant calculator...

The principle is quite simple: for every method you write, the "calculator" tells you what "outside" variable are modified. Obviously it seems quite simple with FP... but not so simple with object/imperative language as soon as you start to call other procedures or subsystems or syscall!

Of course, it could be nice that this "calculator" works inline (while you write your code) and not afterwards (when the program is compiled). It should be "smart enough" for example to tell you that your code is calling an INSERT on a database in a sub-sub-sub procedure of your code or that it is effectively calling some file writing somewhere in the called path

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

#128

Post by api » Sun, Jul 04, 2021, 9:59 PM UTC

macintux wrote: post #87

garethrowlands wrote: post #60

Earlier quoted context omitted.

What is the right problem? What would you _like_ Rust to be solving?

Erlang addresses the memory safety problem to my satisfaction. I'm not eager to embrace the verbosity of a language like Rust until we get closer to a guarantee that if code compiles, it's logically correct as well as safe.

The latter is not possible without some kind of strong AI. The compiler can’t know your intention.

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

#129

Post by macintux » Mon, Jul 05, 2021, 12:04 AM UTC

api wrote: post #128

macintux wrote: post #87

Earlier quoted context omitted.

Erlang addresses the memory safety problem to my satisfaction. I'm not eager to embrace the verbosity of a language like Rust until we get closer to a guarantee that if code compiles, it's logically correct as well as safe.

The latter is not possible without some kind of strong AI. The compiler can’t know your intention.

Then I’ll be waiting a while!

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

#130

Post by liketochill » Mon, Jul 05, 2021, 2:10 AM UTC

test_epsilon wrote: post #100

liketochill wrote: post #97

Earlier quoted context omitted.

Engineering is about the application of science, about safeguarding the public welfare, the duty owed to your clients, and through liability standing behind the work that an engineer does. The modern software industry doesn’t fit that pattern, eula’s shirk all responsibility and dark patterns are applied to trick users. Until people writing software are taking ethics courses and are part of a professional organizatio…

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 relationships, and definitely that has colored my view of what a professional engineer should be.