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

91–100 of 135 posts

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

#91

Post by galangalalgol »

toast0 wrote: post #54
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…

Building construction is full of last minute changes too, it's just that the scope is usually more limited. But a lot of that also boils down to the cost to make changes. You better get the foundation of your 100 story tower right, because it's a big, costly pain to fix it later. When update costs and consequences of errors are similarly high in software, you see real effort spent on getting it right before shipping.…

I've seen plenty of specifications, and they were almost all wrong to a signiy degree. We didn't even know what was possible much less which algorithm was right until we tried it to see. We rewrote it three times using previous iterations only as copy-paste fodder before we liked how it handled real inputs. Then we updated the specification. I like this method.

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

#93

Post by notriddle »

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

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

#94

Post by creata »

libraryofbabel wrote: post #58
pydry wrote: post #27

Where the risk of building the thing wrong is outweighed by the risk of building the wrong thing then formal methods make no sense.

This is the essence of it. Formal methods could be useful when requirements are clear, can be strictly defined, aren't going to change suddenly, and the stakes of building it wrong are very high . Avionics. Medical devices. Cars. Some kinds of embedded systems. Core parts of OS Kernels, databases, network stacks, cryptography libraries, etc. Most software in the world is not like this. It exists to support businesses…

> The issues are fixed and life goes on.

Some bugs can't be fixed: once you've leaked millions of people's personal information, you can't really take it back. The "stakes of building it wrong" are very high in most software, because businesses are all too willing to hoover up all your info.

> The risk to those businesses of even rather bad bugs is generally low.

That is unfortunately true, but hopefully we'll eventually manage to hold businesses accountable for their screwups.

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

#95

Post by SkyMarshal »

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 sanitation via type-checking and similar safeguards may suffice.

But that's closer to formal methods than most of the web dev industry is accustomed to.

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

#96

Post by tsimionescu »

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…

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.

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

#97

Post by liketochill »

test_epsilon wrote: post #85
tralarpa wrote: post #32

Earlier quoted context omitted.

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

No it's not. Engineering does not mean proving a design against a model, although that can be part of engineering (and software has formal proving methods, I might add). Physical engineering projects are not mathematically proven either. They are verified against some accepted set of tests using models that use various empirically measured properties for materials and the world around the project as proxies for how t…

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 organization to which they are accountable for being held to some code, there is no software engineering.

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

#98

Post by bhaak »

garethrowlands wrote: post #59
macintux wrote: post #46

Earlier quoted context omitted.

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.

It's not about not crashing. C lacks memory safety, which leads to many bugs, many of which are security vulnerabilities. Memory safe languages such as python or rust just don't have those problems. The vast majority of languages are memory safe but only C is to-the-metal fast. Well, until Rust came along.

The really bad thing about C's memory unsafety is that crashing is pretty random.

Unless you use a plethora of tooling that patches over these shortcomings, wrong C code doesn't crash reliably (and even then it's not finding everything, only most bugs).

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

#99

Post by sakoht »

"Wouldn't it just be grand if we could write a spec for some piece of code, then let the machines do the rest?"

This is quite possible, if you write the "spec" in a programming language: i.e. write a test case. The problem is that people imagine a formal proof in, for example, English, being simpler or easier to think about than in, say, Python or C. In general this is not true. In general, moment you expect your "spec" (code) to be sufficiently precise for a machine to act upon it, the simplest way to describe it is a programming language.

And if you can invent a better way to describe it, and it is unambiguous enough for a machine to act on it, you've invented a new programming language.

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

#100

Post by test_epsilon »

liketochill wrote: post #97
test_epsilon wrote: post #85

Earlier quoted context omitted.

No it's not. Engineering does not mean proving a design against a model, although that can be part of engineering (and software has formal proving methods, I might add). Physical engineering projects are not mathematically proven either. They are verified against some accepted set of tests using models that use various empirically measured properties for materials and the world around the project as proxies for how t…

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 mechanical engineering in automobiles. If you've spent much time around cars, you'll know that they have a lot of quirks like this where it's obvious a problem has been found and fixed. For example an engine of a particular vintage might be known to be prone to head cracking, then a few years later they might come out with another engine with a lot of the same part numbers but revised head design or material.

The engineers who designed it were not gazing at idealized otto cycle equations or out polling the public about its welfare, and the company behind it was doing its level best to play down the problem and coming up with ways their dealers could try to nurse cars through their warranty periods.

Post reply on HN