I wrote a (dummy) paper for a class about automatically generating a formal specification based on a given program using a GAN. I don't really know how feasible it would be, but I feel like that would circumvent some of the issues being brought up in the comments about how difficult it is for organizations to use formal methods in their workflows.
Where are we going from here? Software engineering needs formal methods
21–30 of 135 posts
Re: Where are we going from here? Software engineering needs formal methods
#22Code is already a formal specification of sorts. I'm sure more rigor will lead to fewer errors, it also will increase development time, which is a poor tradeoff in many domains. Plus, a source of many bugs is that the specification is wrong, which will remain true even if rigor is increased.
Edit: Of course there is low hanging fruit that can be incorporated into languages. I write a lot fewer bugs in C++ than I do in C and a lot fewer in Swift than I do in C++.
Re: Where are we going from here? Software engineering needs formal methods
#23The 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.
Doing the wrong thing is almost always worse than crashing.
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.
Re: Where are we going from here? Software engineering needs formal methods
#24It 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 spurious counterexamples. And remember that essential complexity is in specifying a system? Now try to specify something as simple as quicksort. Let’s just say specifying a system with mathematical logic is beyond 99.99% of software engineers. Not that people are incapable, but I doubt people have enough incentive to swallow the cost. For one, how much does it cost to debug a spec? Don’t believe me, do try out the book by Hehner: http://www.cs.utoronto.ca/~hehner/FMSD/, or introductory books like this: https://www.amazon.com/Verification-Reactive-Systems-Algorit..., and you’ll get the idea. And yes, I thoroughly studied the mentioned books cover to cover and still think they are not for the majority of software engineers.
Re: Where are we going from here? Software engineering needs formal methods
#25There are plenty of shops that apply rigorous, formal methods to software design. Military contractors providing software for mission critical systems do this (or used to). Some will cut corners, but they are supposed to follow the methods and procedures the contracts specify. It isn’t common in private industry because it’s typically deemed unimportant.
You aren't paid either to write unit tests in the private industry. You are paid to write working code.
You'd be surprised. Often, the tests are more work than the "working code" itself. At companies that have a test heavy focus, I'd say roughly 50% or 60% of the effort is spent on tests (this includes future work to maintaining tests as they are affected by other areas of the code, etc.) You may not be able to get your PR approved without enough tests.
Re: Where are we going from here? Software engineering needs formal methods
#26Earlier quoted context omitted.
Doing the wrong thing is almost always worse than crashing.
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?
Re: Where are we going from here? Software engineering needs formal methods
#27Where the risk of building the thing wrong is outweighed by the risk of building the wrong thing then formal methods make no sense.
Re: Where are we going from here? Software engineering needs formal methods
#28(1990)
Re: Where are we going from here? Software engineering needs formal methods
#29Earlier 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?
Ok, now I see the point of confusion.
Erlang is my go-to language when I have the freedom to choose, and it is explicitly designed to crash when there's a mismatch between the expected and current state.
So, I was indeed missing the point of the statement.
Re: Where are we going from here? Software engineering needs formal methods
#30Software isn’t a special unique snowflake as some developers, who have never worked in other fields, will tell you. Software certainly seems unique though when you have no other professional employment experience to compare it to.
The primary problem with missing formal methods is supplemental guidance bolted on artificially in search of a problem producing some canned solution. The reason for that people tend to focus on their personal needs instead of business needs. For example many developers will suggest an approach of personal familiarity even if it costs more, performs poorly, and lowers product quality. Furthermore many developers tend to focus on composition and tools first as opposed to saving composition for the final step and using either no tools or a more correct tool for the job.
Formal methods on the other hand provide guidance for a planning process that articulates the work to be performed opposed to how that work should be done.