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

61–70 of 135 posts

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

#61

Post by takeda »

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.

With interpreted languages it is trivial, you just try parts of your code. For python there's for example ipython which makes the experience really great.

Also I don't agree with GP, there are places that require unit tests, especially if multiple people are working on a project. You could be a developer that never made a bug in your life, but others might not be as great :) besides many bugs also happen by changing other parts of the code. Some of your assumptions might have been 100% correct when you wrote the code, but someone can change different part of the code and now your function is called with values that were previously impossible.

The great thing about statically typed languages is that they might detect large part of these bugs, but you're out of luck with dynamically typed languages.

Example of this was the Python 2 -> Python 3 migration. Having a large test suite helped tremendously.

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

#62

Post by MaxBarraclough »

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

Depends on jurisdiction. In the UK anyone can call themselves a software engineer.

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

#64

Post by lostcolony »

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…

Yep. Anyone who tries to do that in a competitive space will have their lunch eaten by people who slap something together and get it in front of customers.

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

#65

Post by zozbot234 »

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 relatively simple ways, and would benefit more from an end-to-end system that establishes valuable properties (even comparatively trivial ones like type and memory safety, or simple pre- and post-conditions) about the actual code one will be executing.

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

#66

Post by analog31 »

trinovantes wrote: post #53
wikibob wrote: post #43

Earlier quoted context omitted.

Says who?

It's a protected job title in most state/provincial governments For example, "In Ontario, the titles 'engineer' and 'professional engineer' are restricted by law ... When individuals are found to be using the restricted title 'engineer,' the courts can impose fines, restraining orders and jail time" [1]. It's just hardly reported/enforced in the software industry because most "software engineers" do not work on thing…

In most US states, there is a broad "industrial exemption" for engineers who work for an employer.

https://peimpact.com/pe-industrial-exemption/

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

#67

Post by [deleted] »

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…

[deleted]

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

#68

Post by zozbot234 »

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?

Rust programs can fail gracefully when they hit unexpected conditions - Safe Rust guarantees only extend to memory- and data-race safety. However, these tend to be table-stakes if one wants to make any kind of interesting statement about the semantics of programs, and there's a lot of ongoing work wrt. enabling this kind of use of Rust.

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

#69

Post by deregulateMed »

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?"

Subjective, and impossible to come up with a single, undebatable correct answer.

As opposed to, "What metal should we choose for this wire harness?" With cost and quality metrics, there's only 1 correct answer.

Making a clear cut distinction between engineering and programming would do literal wonders for programming. Anything deemed SWE should be objectively correct. Anything else would be free to be scrutinized by Art, Tradition, Science, and Authority.

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

#70

Post by spc476 »

bhaak wrote: post #14
sidlls wrote: post #8

Earlier quoted context omitted.

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

I agree, automatic testing would be nice. Unfortunately, I'm the one at work having to do write the said automatic testing of a component that makes parallel DNS requests [1] in an event driven server [2] and need to test that we cover the case where A returns, then B, and B returns, then A, A returns, B returns after our timeout [3], B returns, A returns after our timeout, A returns, B never does, B returns, A never does, while at the same time, making sure the ping tests (the components send a known query to each server to ensure each server is still available [4]) go through because if they don't that particular server will be taken out of rotation. God, I would love to have that automatically tested. What I don't like is having to automate such tests.

[1] To different servers that return different information for a given query. The protocol happens to be DNS.

[2] Based upon poll(), epoll() or kqueue(), depending upon the platform.

[3] We're under some pretty tight time constraints for our product.

[4] DNS, over UDP.

Post reply on HN