[HN Gopher] Where are we going from here? Software engineering n...
___________________________________________________________________
Where are we going from here? Software engineering needs formal
methods
Author : ntietz
Score : 52 points
Date : 2021-07-03 19:54 UTC (3 hours ago)
(HTM) web link (ntietz.com)
(TXT) w3m dump (ntietz.com)
| rebelos wrote:
| Whether or not formal methods can be applied is almost entirely
| an economic decision since that kind of rigor drives up cost.
| Makes sense in certain high value systems when the organization
| wrapped around them has the resources or the level of risk
| associated with a less rigorous approach is too high (e.g. at
| NASA).
|
| What the author seems to miss completely is that there are many
| systems developed using typical methodologies that generate
| billions in revenue. What this tells you is that ideas like TLA+
| are effectively superfluous in a wide variety of software
| contexts.
| bhaak wrote:
| It's not easy to quantify but you can't just dismiss formal
| methods because we don't know how much development and
| maintenance overhead they would eliminate.
|
| How much revenue something generates is a poor metric.
| Otherwise, we all would probably be programming in PHP.
| bobthechef wrote:
| I don't think the OP dismisses formal methods, only the idea
| that they have pervasive utility that outweighs costs in most
| scenarios, at least for certain kinds of formal methods.
|
| But we can't forget the range of formal methods either. Type
| systems technically qualify, as the article notes, even if
| they are lightweight, and they're not new. Given the
| pervasiveness of Java, we're already making widespread use of
| at least that formal method and have been for a long time.
|
| > How much revenue something generates is a poor metric.
| Otherwise, we all would probably be programming in PHP.
|
| The OP wasn't arguing that revenue is driving or should drive
| language selection, only that the revenue shows that the lack
| of formal methods does not seems to prevent companies from
| making enormous sums of money.
|
| > you can't just dismiss formal methods because we don't know
| how much development and maintenance overhead they would
| eliminate.
|
| That by itself is not much of a positive argument for their
| use. And do you know how much maintenance overhead they would
| introduce? In either case, it might be useful to compare how
| a switch between similar languages (e.g. JS and Typescript)
| affected code quality (in terms of the number of bug reports
| filed, for example) and feature delivery time. Maybe there's
| a point where the trade off makes sense. In which case,
| languages that support a gradual adoption of formal methods
| might begin to look attractive.
| oneplane wrote:
| The programming language itself has very little to do with
| the revenue something generates.
|
| Revenue isn't generated by technical details, those are just
| the implementation of a product that itself is just an
| implementation of the goals of the business.
|
| The reason people are and aren't programming in PHP is just
| plain and simple: taste. Maybe ff 10 developers in a team
| want to use PHP they can just do that, as long as at the end
| of the line the product delivers. If 3/10 want to use PHP,
| and 7/10 want to use C# then no, it will not likely run on
| PHP. And if as a developer you prefer certain features or
| tools over others, you are likely to select the technologies
| that suit that.
|
| None of the technical details had anything to do with the
| value that was created.
|
| If your requirements say that 100 people per minute need to
| be able to find, basket and purchase product on a website,
| and those requirements are met, does it really matter if the
| codebase is a combination of AppleScript and an ActiveX
| control? (I know, that technically doesn't exist, not the
| point)
|
| Now, if those requirements also include scaling needs, long-
| term support needs, knowledge sharing, consultancy options,
| then you might not select those technologies.
| ntietz wrote:
| I mean, it depends on criticality. If something is critical,
| pushing further along the formal methods spectrum makes sense
| (see also: why AWS has done a lot with TLA+). Sure, we probably
| won't verify all of Instagram, but super critical portions of
| the platform underlying it are likely worth it and would save
| money in the long run by reducing outages, bugs, etc.
| api wrote:
| The 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.
| macintux wrote:
| Doing the wrong thing is almost always worse than crashing.
| bhaak wrote:
| 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.
| macintux wrote:
| 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?
| boustrophedon wrote:
| 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.
| macintux wrote:
| 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.
| totemandtoken wrote:
| 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.
| jeffreyrogers wrote:
| Code 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++.
| sidlls wrote:
| There 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.
| bhaak wrote:
| You aren't paid either to write unit tests in the private
| industry.
|
| You are paid to write working code.
| ironman1478 wrote:
| 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.
| icedchai wrote:
| 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.
| sidlls wrote:
| 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.
| j1elo wrote:
| Do you know of any formal study that talks about this?
| bhaak wrote:
| 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 found with
| manual testing before they go into production.
| FpUser wrote:
| I once had this fun contract to fix code in one giant
| application written in PHP. The org of decent size who
| wrote said code in a first place had code reviews, unit
| tests and what not.
|
| The end result was that they had to hire outside person to
| fix what they have produced. I looked through the software
| and noticed whole bunch of iffy patterns. Ended up writing
| giant Python script that searched said patterns and fixed
| it where possible marking with appropriate comments and
| issued a warning comments where it could not.
|
| Not sure if this is a regular occurrence in companies that
| write and maintain their internal software as this was the
| only time I did job like this.
| ntietz wrote:
| There's a spectrum of formal methods and with the push toward
| static types in Python coming directly out of industry I would
| argue that industry is definitely deeming it important in some
| degree; the question is to what degree. Right now a lot of the
| time it's only worth it for the most critical systems (S3, for
| example, but not my side project webapp) but if tooling
| improved, it would be worth it for more cases.
| werpon wrote:
| Formal methods may work for civil engineering where the usual
| workflow is gathering requirements, developing a detailed project
| and building the thing, with the implicit understanding that any
| little change will mean recalculating costs and deadlines.
|
| When your customer decides to pivot the fintech app you were
| developing into a cryptocurrency investment tool, it makes no
| sense.
| bhaak wrote:
| How much help your unit tests if your customer pivots from
| their original idea?
|
| Is that a reason not to write unit tests in the first place?
| nextos wrote:
| That's a bit extreme. In cases where things move quite quickly,
| we should still be able to provide some formal guarantees.
| There's a whole spectrum of formal methods ranging from formal
| proofs to rich type systems and design by contract.
|
| I have personally had a lot of success with some techniques,
| and I'm quite hopeful ideas such as those in Liquid Haskell
| will eventually become mainstream.
| [deleted]
| j1elo wrote:
| 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 wouldn't be a bad thing that the same thing happens,
| to a lesser extent, in Software Engineering. Say bye to stupid
| last minute changes caused by the fact that they are not
| perceived as expensive, and all the bad incentives it creates
| in the people writing that software.
| tralarpa wrote:
| 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
| :)
| hluska wrote:
| This is some absolutely amazing writing. Good heavens, your
| line about debating whether a hammer or a saw is the right
| tool for inserting a screw?? Beautiful!!
|
| Do you blog? If so, I'd love to read more of you. If not,
| again, this is some seriously good writing. Big, end of a
| long drunken night "I really love you man, woman or
| whatever" ups!!!
| colordrops wrote:
| It would be a bad thing though. The fact that software is
| changed with so little effort is a feature and a positive
| aspect. The only thing that should factor into whether a more
| rigorous approach should be taken is the use case.
| hintymad wrote:
| 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 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.
| pydry wrote:
| Where the risk of building the thing wrong is outweighed by the
| risk of building the wrong thing then formal methods make no
| sense.
| andrewnicolalde wrote:
| Brilliantly put.
| paiute wrote:
| people forget that we tried this and it didn't really work out
| that well. gang of four is only mildly useful.
| allyourhorses wrote:
| (1990)
| kolinko wrote:
| There is a lot of formal method usage in smart contracts. Maker
| DAO for example did a full formal verification of their stuff,
| and there is a lot of talk within the security community about
| it.
| ntietz wrote:
| Yes! The blockchain community is doing a lot of cool stuff here
| and it's definitely an area where it's worth it even with less
| than ideal tools.
| austincheney wrote:
| Software 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.
| markus_zhang wrote:
| Comparing to real engineering, I really don't think we can even
| get close in regarding to project management and expectation
| handling.
|
| Plus actually real projects frequently go over their budget (by a
| huge margin), go over their planned time, or go totally wrong.
| fridif wrote:
| No it does not. Please do not turn software engineering into yet
| another needlessly licensed profession, it has already been
| tried.
| 8note wrote:
| Software development*
|
| If you want to call yourself an engineer; the licensing is
| essential
| wikibob wrote:
| Says who?
| m_j_g wrote:
| Contrary, formal methods could (in theory!!) give as way to
| assess correctness of software regardless of programmer
| qualifications.
___________________________________________________________________
(page generated 2021-07-03 23:00 UTC)