13 ms·

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

139 points by ntietz 5y ago

rebelos 5y ago
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 5y ago
  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 5y ago
    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 5y ago
    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 5y ago
  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.
  - MaxBarraclough 5y ago
    I'm fond of formal methods, but I'll offer the usual counter-example: Formal methods struggle to scale up to real-world problems. There is no formally verified TCP/IP stack. There is no formally verified TLS or SSH implementation. That's despite how immensely useful and reusable such implementations could be (that is to say, high demand, and yet no supply). As I understand it we're not even close to being able to develop a formally verified TLS implementation, but if we were, it would likely take the form of an internationally acclaimed PhD thesis, akin to CompCert. It still wouldn't mean formal methods are cheap and easy.
    - TheOtherHobbes 5y ago
      It's astounding that core security infrastructure isn't formally designed and certified, and isn't available as standardised - certified - drop-in elements. A top decile PhD thesis is not a high bar in engineering. It's how most disciplines evolve. "Not invented here" is not a credible explanation for why CS feels a need to be different.
- andrekandre 5y ago
  also, they dont mean bunk if business side of the equation isnt behind them... following formal methods means that business also follows formal business methods (which would reduce sudden changes and mistaken product designs etc). too many times "dev" is treated like a roving circus that can just change their routine on a dime with little consequences...
sidlls 5y ago
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 5y ago
  You aren't paid either to write unit tests in the private industry. You are paid to write working code.
  - sidlls 5y ago
    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 5y ago
      Do you know of any formal study that talks about this?
      - sidlls 5y ago
        It's pretty easy to find various papers/studies about TDD, unit testing, and the like by searching online but I would not call any of them scientifically or empirically rigorous. Given the lack of any objective or agreeable standards regarding what "code quality" means, these papers can draw conclusions to support any view.
    - bhaak 5y ago
      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.
werpon 5y ago
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 5y ago
  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?
  - hwayne 5y ago
    Generally unit testing is faster than formal verification, so you're out less work if requirements change.
- deleted 5y ago
  [deleted]
- j1elo 5y ago
  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.
  - colordrops 5y ago
    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.
kolinko 5y ago
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 5y ago
  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.
api 5y ago
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 5y ago
  Doing the wrong thing is almost always worse than crashing.
  - bhaak 5y ago
    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 5y ago
      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?
      - macintux 5y ago
        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.
      - boustrophedon 5y ago
        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.
totemandtoken 5y ago
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 5y ago
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++.
hintymad 5y ago
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/ http://www.cs.utoronto.ca/~hehner/FMSD/, or introductory books like this: https://www.amazon.com/Verification-Reactive-Systems-Algorithms-Theoretical/dp/3540002960 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.
- lostcolony 5y ago
  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.
- zozbot234 5y ago
  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.
  - pron 5y ago
pydry 5y ago
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 5y ago
  Brilliantly put.
- paiute 5y ago
  people forget that we tried this and it didn't really work out that well. gang of four is only mildly useful.
- libraryofbabel 5y ago
  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 trying to make a buck in a changing world, either from consumers or from other businesses. Requirements are messy, shift frequently, and agreeing on what they are at all is more than half the battle. Nobody really knows the minutiae of quite how the whole product works but it doesn't really matter. Money is still coming in. The risk to those businesses of even rather bad bugs is generally low. A few customers have a bad day because they see a 500 error in their browser when they're trying to order food, or they can't summon their ride-share for 5 minutes. The issues are fixed and life goes on. The perfection of formal methods is the enemy of good, and would be a net negative return on investment, much as programmers who (understandably) love perfection and clarity and rigor might want it to be otherwise.
  - AlotOfReading 5y ago
    We all make use of those components though, regardless of how CRUD the application is. We'd all benefit from them being validated. The fact that "fully validated" versions of those components don't exist is simultaneously an indication of how difficult the problem is and how little our industry truly cares about product reliability and quality. These issues are not rare or even particularly uncommon in the wild. I imagine the pursuit of formal methods in software that doesn't strictly require it would go a long way to fixing other systemic issues like tech debt, security, and performance.
allyourhorses 5y ago
(1990)
- effie 5y ago
  So true.
austincheney 5y ago
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 5y ago
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 5y ago
No it does not. Please do not turn software engineering into yet another needlessly licensed profession, it has already been tried.
- 8note 5y ago
  Software development* If you want to call yourself an engineer; the licensing is essential
  - wikibob 5y ago
    Says who?
    - trinovantes 5y ago
      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 things that affect public safety or can result in loss of life. [1] https://www.peo.on.ca/engineering-licensing-body-clarifies-use-term-engineer-following-reported-dismissal-hydro-one https://www.peo.on.ca/engineering-licensing-body-clarifies-u...
      - analog31 5y ago
        In most US states, there is a broad "industrial exemption" for engineers who work for an employer. https://peimpact.com/pe-industrial-exemption/ https://peimpact.com/pe-industrial-exemption/
  - MaxBarraclough 5y ago
    Depends on jurisdiction. In the UK anyone can call themselves a software engineer.
  - effie 5y ago
hyperpallium2 5y ago
These days, coding is the quickest way to find out what's needed. That is: implementation precedes requirements. This is the real reason software is eating the world. Incumbents lose because aren't able to reorganize themselves around a software core, and so can't try things. Formal methods are intrinsically satisfying, as are all quests for perfection and truth.
zozbot234 5y ago
Relevant blogpost series from hillelwayne: The Crossover Project - Are We Really Engineers? https://www.hillelwayne.com/tags/crossover-project/ https://www.hillelwayne.com/tags/crossover-project/
deregulateMed 5y ago
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.
- notriddle 5y ago
  https://www.hillelwayne.com/post/crossover-project/are-we-really-engineers/ https://www.hillelwayne.com/post/crossover-project/are-we-re...
  - deregulateMed 5y ago
    That article proved nothing.
effie 5y ago
> But as a goal, that's really what you want: we want to solve the problem by saying "this is the solution" and then poof the solution appears! Actually, that is very often not the case. Many SW projects start with an idea of what the software should do, but there is no easy way to describe it in full detail. Writing down the complete specification right from the start would be very hard and prone to wasted work. For example, say you want to write a messaging system. You could try to imagine the whole thing and describe it in some formal language, but this will most often produce huge pile of ideas that weren't tested and are not part of desired solution in the end. It's too much "building in the head". Instead, we should prototype. We write the simplest possible thing that roughly does what we want, and then add and remove features as convenient/needed and improve various characteristics. We handle corner cases as they appear, sometimes learn that something new has to be studied / understood first, and some parts that have been written have to be rewritten and then we do so. Writing the spec for the result may be done in the end, after the software is done and works and the ideas are proven to work.
solarmist 5y ago
I think the way software will evolve into a more traditional engineering role will be in layers of abstraction starting closest to the hardware. Which will become certified services/systems to build more loosely on top of or using as components. We’re starting to see this with commoditization/formalization of platforms. OS, storage, cloud, infrastructure, e-commerce are getting to the point where they’re pretty well explored. In another 20 years it’ll be so specialized and optimized that you’d need a Ph.D to make meaningful improvements in those areas. So people won’t feel the need to try and recreate it themselves except for learning and as that process continues we’ll see those things formalize best practices which would eventually turn into engineering standards, etc… You’ll have licensed and bonded engineers building low level highly formalized systems/services which meet certain guarantees. Similar to how I imagine civil engineering works. Then for the rest of the industry you’ll have what we currently have which is like home construction where almost anything goes, but there are pieces that need to be validated by actual engineers or licensed professionals similar to how electricians and plumbers are licensed.
cratermoon 5y ago
Funny, I was just re-reading this today and thinking about how the industry has played out in the twenty years since. http://www.mcs.vuw.ac.nz/comp/Publications/CS-TR-02-9.abs.html http://www.mcs.vuw.ac.nz/comp/Publications/CS-TR-02-9.abs.ht...
madrox 5y ago
I’ve once thought this way, but over the years I’ve come to decide that such formalization will never outpace frameworks. Frameworks are easier to grok and scale better than rigorous education.
pw262 5y ago
For business applications, formal methods are really limited to core algorithms. The real problem is that data entry and validation should be a solved problem. Sadly this is not the case. Try using .Net WPF or React and your only recourse is to Stack Overflow. These frameworks are over complicated and are full of weird edge cases that make everyday programming tedious and error prone. Lets get our house in order before we break out the temporal logic.
valenterry 5y ago
Is there even a good definition of "engineering" somewhere? The one from Wikipedia for example is not really great imho, as it can be interpreted to be applicable to almost every job.
sakoht 5y ago
"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.
cryptos 5y ago
I think a sweet spot is "specification by example" also called behavior driven development (BDD). You take a more or less standardized, but human readable language to write down the specification and implement test adapters for it. A typical tool for this approach would be Cucumber: https://cucumber.io/ https://cucumber.io/
- cloogshicer 5y ago
  Having done BDD at work, I can only say it's not the right approach. The "human-readableness" of the test cases produced with BDD is debatable - at least at our company only technical people familiar with the code could understand the spec. At the same time BDD was very cumbersome to do, while not really providing us any benefits.
ud_0 5y ago
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 initiatives. The notion that software engineering should be grouped under civil engineering is misguided. Part of the reason why we're looking to other fields is to profit from their experience (which is good) but part of it is also because we're desiring a kind of legitimacy we feel is absent. It's a reasonable impulse to a degree, for smart people dedicating their productive years to a discipline. We want to do a good job. The problem is that we have more in common with architects than we do with civil engineers. There are some goals that can be measured with a boolean outcome: does the code compile, is a certain algorithm provably correct given certain conditions, can a building be built. But it gets murky very very quickly: how well does a thing we create serve its purpose? Does it use resources efficiently? How long will a structure last? What kind of adverse conditions will bring it down? Does the thing make people's lives better and if so by what measure? These are a small hint at the questions where formal methods tend to fall down or even work against us. So do we need overarching formal methods or do we need to be more scientific about specific objectives and measurement of outcomes that are important to us subjectively?
- Taek 5y ago
  I think it depends on what you are building. For example, if you are building a database that houses user data and user credentials, this is is a very well understood thing that experienced professionals can set up quickly, efficiently, and give you both a lot of security and also enough flexibility to build whatever business you want behind it. And yet, it seems that most companies and websites that handle user credentials do a poor job at it. So there does seem to be an argument in favor of adding formal methods in certain areas of software design and engineering. One thing that very much distinguishes the software world from every other type of engineering is the complexity and rate of innovation. In software, I can invent and deploy a thing on the same day and the total R&D cost to my company is almost exactly equal to my salary for that day. Whereas for something like a bridge, the R&D cycle for a new bridge invention could be several months and hundreds of thousands of dollars for a similar idea. Overall, I think the discussion about putting standards in place for certain common activities (network communications, password databases, encryption standards, and similarly well understood areas) is worth having. Though I also would be concerned that state actors would use such standardization to insert weaponized requirements like backdoors, or that regulation would prevent new innovations from gaining a foothold.
pjmlp 5y ago
Very unwelcome opinion around here. We could start by stop calling software engineering to 6 months coding bootcamps, letting it for actual 5 years experience being taught correct engineering practices and respective skill assessment. Then we can start talking about adopting what is still missing from real engineering practices into the field. Ah, and in the process make companies liable for skipping quality control when everything goes wrong.
skneko 5y ago
I am a research intern working in a group studying and developing formal methods. The tech we are working with has served to verify planes, trains and has been used in NASA. AMA if anyone here is curious about how the world around FM works.
jalcazar 5y ago
Program verification is an expensive activity. Navigating the cost-benefit trade-off of program verification is ultimately a business decision. https://t.co/IUCLtDLROC https://t.co/IUCLtDLROC
olivierduval 5y ago
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

139 points by ntietz 5y ago

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 5y ago
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 5y ago
  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 5y ago
  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 5y ago
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.
- MaxBarraclough 5y ago
  I'm fond of formal methods, but I'll offer the usual counter-example: Formal methods struggle to scale up to real-world problems. There is no formally verified TCP/IP stack. There is no formally verified TLS or SSH implementation. That's despite how immensely useful and reusable such implementations could be (that is to say, high demand, and yet no supply). As I understand it we're not even close to being able to develop a formally verified TLS implementation, but if we were, it would likely take the form of an internationally acclaimed PhD thesis, akin to CompCert. It still wouldn't mean formal methods are cheap and easy.
  - TheOtherHobbes 5y ago
    It's astounding that core security infrastructure isn't formally designed and certified, and isn't available as standardised - certified - drop-in elements. A top decile PhD thesis is not a high bar in engineering. It's how most disciplines evolve. "Not invented here" is not a credible explanation for why CS feels a need to be different.
andrekandre 5y ago
also, they dont mean bunk if business side of the equation isnt behind them... following formal methods means that business also follows formal business methods (which would reduce sudden changes and mistaken product designs etc). too many times "dev" is treated like a roving circus that can just change their routine on a dime with little consequences...

sidlls 5y ago

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 5y ago
You aren't paid either to write unit tests in the private industry. You are paid to write working code.
- sidlls 5y ago
  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 5y ago
    Do you know of any formal study that talks about this?
    - sidlls 5y ago
      It's pretty easy to find various papers/studies about TDD, unit testing, and the like by searching online but I would not call any of them scientifically or empirically rigorous. Given the lack of any objective or agreeable standards regarding what "code quality" means, these papers can draw conclusions to support any view.
  - bhaak 5y ago
    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.

werpon 5y ago

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 5y ago
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?
- hwayne 5y ago
  Generally unit testing is faster than formal verification, so you're out less work if requirements change.
deleted 5y ago
[deleted]
j1elo 5y ago
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.
- colordrops 5y ago
  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.

kolinko 5y ago

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 5y ago
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.

api 5y ago

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 5y ago
Doing the wrong thing is almost always worse than crashing.
- bhaak 5y ago
  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 5y ago
    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?
    - macintux 5y ago
      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.
    - boustrophedon 5y ago
      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.

totemandtoken 5y ago

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 5y ago

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

hintymad 5y ago

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/ http://www.cs.utoronto.ca/~hehner/FMSD/, or introductory books like this: https://www.amazon.com/Verification-Reactive-Systems-Algorithms-Theoretical/dp/3540002960 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.

lostcolony 5y ago
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.
zozbot234 5y ago
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.
- pron 5y ago

pydry 5y ago

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 5y ago
Brilliantly put.
paiute 5y ago
people forget that we tried this and it didn't really work out that well. gang of four is only mildly useful.
libraryofbabel 5y ago
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 trying to make a buck in a changing world, either from consumers or from other businesses. Requirements are messy, shift frequently, and agreeing on what they are at all is more than half the battle. Nobody really knows the minutiae of quite how the whole product works but it doesn't really matter. Money is still coming in. The risk to those businesses of even rather bad bugs is generally low. A few customers have a bad day because they see a 500 error in their browser when they're trying to order food, or they can't summon their ride-share for 5 minutes. The issues are fixed and life goes on. The perfection of formal methods is the enemy of good, and would be a net negative return on investment, much as programmers who (understandably) love perfection and clarity and rigor might want it to be otherwise.
- AlotOfReading 5y ago
  We all make use of those components though, regardless of how CRUD the application is. We'd all benefit from them being validated. The fact that "fully validated" versions of those components don't exist is simultaneously an indication of how difficult the problem is and how little our industry truly cares about product reliability and quality. These issues are not rare or even particularly uncommon in the wild. I imagine the pursuit of formal methods in software that doesn't strictly require it would go a long way to fixing other systemic issues like tech debt, security, and performance.

allyourhorses 5y ago

(1990)

effie 5y ago
So true.

austincheney 5y ago

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 5y ago

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 5y ago

No it does not. Please do not turn software engineering into yet another needlessly licensed profession, it has already been tried.

8note 5y ago
Software development* If you want to call yourself an engineer; the licensing is essential
- wikibob 5y ago
  Says who?
  - trinovantes 5y ago
    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 things that affect public safety or can result in loss of life. [1] https://www.peo.on.ca/engineering-licensing-body-clarifies-use-term-engineer-following-reported-dismissal-hydro-one https://www.peo.on.ca/engineering-licensing-body-clarifies-u...
    - analog31 5y ago
      In most US states, there is a broad "industrial exemption" for engineers who work for an employer. https://peimpact.com/pe-industrial-exemption/ https://peimpact.com/pe-industrial-exemption/
- MaxBarraclough 5y ago
  Depends on jurisdiction. In the UK anyone can call themselves a software engineer.
- effie 5y ago

hyperpallium2 5y ago

These days, coding is the quickest way to find out what's needed. That is: implementation precedes requirements. This is the real reason software is eating the world. Incumbents lose because aren't able to reorganize themselves around a software core, and so can't try things. Formal methods are intrinsically satisfying, as are all quests for perfection and truth.

zozbot234 5y ago

Relevant blogpost series from hillelwayne: The Crossover Project - Are We Really Engineers? https://www.hillelwayne.com/tags/crossover-project/ https://www.hillelwayne.com/tags/crossover-project/

deregulateMed 5y ago

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.

notriddle 5y ago
https://www.hillelwayne.com/post/crossover-project/are-we-really-engineers/ https://www.hillelwayne.com/post/crossover-project/are-we-re...
- deregulateMed 5y ago
  That article proved nothing.

effie 5y ago

> But as a goal, that's really what you want: we want to solve the problem by saying "this is the solution" and then poof the solution appears! Actually, that is very often not the case. Many SW projects start with an idea of what the software should do, but there is no easy way to describe it in full detail. Writing down the complete specification right from the start would be very hard and prone to wasted work. For example, say you want to write a messaging system. You could try to imagine the whole thing and describe it in some formal language, but this will most often produce huge pile of ideas that weren't tested and are not part of desired solution in the end. It's too much "building in the head". Instead, we should prototype. We write the simplest possible thing that roughly does what we want, and then add and remove features as convenient/needed and improve various characteristics. We handle corner cases as they appear, sometimes learn that something new has to be studied / understood first, and some parts that have been written have to be rewritten and then we do so. Writing the spec for the result may be done in the end, after the software is done and works and the ideas are proven to work.

solarmist 5y ago

I think the way software will evolve into a more traditional engineering role will be in layers of abstraction starting closest to the hardware. Which will become certified services/systems to build more loosely on top of or using as components. We’re starting to see this with commoditization/formalization of platforms. OS, storage, cloud, infrastructure, e-commerce are getting to the point where they’re pretty well explored. In another 20 years it’ll be so specialized and optimized that you’d need a Ph.D to make meaningful improvements in those areas. So people won’t feel the need to try and recreate it themselves except for learning and as that process continues we’ll see those things formalize best practices which would eventually turn into engineering standards, etc… You’ll have licensed and bonded engineers building low level highly formalized systems/services which meet certain guarantees. Similar to how I imagine civil engineering works. Then for the rest of the industry you’ll have what we currently have which is like home construction where almost anything goes, but there are pieces that need to be validated by actual engineers or licensed professionals similar to how electricians and plumbers are licensed.

cratermoon 5y ago

Funny, I was just re-reading this today and thinking about how the industry has played out in the twenty years since. http://www.mcs.vuw.ac.nz/comp/Publications/CS-TR-02-9.abs.html http://www.mcs.vuw.ac.nz/comp/Publications/CS-TR-02-9.abs.ht...

madrox 5y ago

I’ve once thought this way, but over the years I’ve come to decide that such formalization will never outpace frameworks. Frameworks are easier to grok and scale better than rigorous education.

pw262 5y ago

For business applications, formal methods are really limited to core algorithms. The real problem is that data entry and validation should be a solved problem. Sadly this is not the case. Try using .Net WPF or React and your only recourse is to Stack Overflow. These frameworks are over complicated and are full of weird edge cases that make everyday programming tedious and error prone. Lets get our house in order before we break out the temporal logic.

valenterry 5y ago

Is there even a good definition of "engineering" somewhere? The one from Wikipedia for example is not really great imho, as it can be interpreted to be applicable to almost every job.

sakoht 5y ago

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

cryptos 5y ago

I think a sweet spot is "specification by example" also called behavior driven development (BDD). You take a more or less standardized, but human readable language to write down the specification and implement test adapters for it. A typical tool for this approach would be Cucumber: https://cucumber.io/ https://cucumber.io/

cloogshicer 5y ago
Having done BDD at work, I can only say it's not the right approach. The "human-readableness" of the test cases produced with BDD is debatable - at least at our company only technical people familiar with the code could understand the spec. At the same time BDD was very cumbersome to do, while not really providing us any benefits.

ud_0 5y ago

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 initiatives. The notion that software engineering should be grouped under civil engineering is misguided. Part of the reason why we're looking to other fields is to profit from their experience (which is good) but part of it is also because we're desiring a kind of legitimacy we feel is absent. It's a reasonable impulse to a degree, for smart people dedicating their productive years to a discipline. We want to do a good job. The problem is that we have more in common with architects than we do with civil engineers. There are some goals that can be measured with a boolean outcome: does the code compile, is a certain algorithm provably correct given certain conditions, can a building be built. But it gets murky very very quickly: how well does a thing we create serve its purpose? Does it use resources efficiently? How long will a structure last? What kind of adverse conditions will bring it down? Does the thing make people's lives better and if so by what measure? These are a small hint at the questions where formal methods tend to fall down or even work against us. So do we need overarching formal methods or do we need to be more scientific about specific objectives and measurement of outcomes that are important to us subjectively?

Taek 5y ago
I think it depends on what you are building. For example, if you are building a database that houses user data and user credentials, this is is a very well understood thing that experienced professionals can set up quickly, efficiently, and give you both a lot of security and also enough flexibility to build whatever business you want behind it. And yet, it seems that most companies and websites that handle user credentials do a poor job at it. So there does seem to be an argument in favor of adding formal methods in certain areas of software design and engineering. One thing that very much distinguishes the software world from every other type of engineering is the complexity and rate of innovation. In software, I can invent and deploy a thing on the same day and the total R&D cost to my company is almost exactly equal to my salary for that day. Whereas for something like a bridge, the R&D cycle for a new bridge invention could be several months and hundreds of thousands of dollars for a similar idea. Overall, I think the discussion about putting standards in place for certain common activities (network communications, password databases, encryption standards, and similarly well understood areas) is worth having. Though I also would be concerned that state actors would use such standardization to insert weaponized requirements like backdoors, or that regulation would prevent new innovations from gaining a foothold.

pjmlp 5y ago

Very unwelcome opinion around here. We could start by stop calling software engineering to 6 months coding bootcamps, letting it for actual 5 years experience being taught correct engineering practices and respective skill assessment. Then we can start talking about adopting what is still missing from real engineering practices into the field. Ah, and in the process make companies liable for skipping quality control when everything goes wrong.

skneko 5y ago

I am a research intern working in a group studying and developing formal methods. The tech we are working with has served to verify planes, trains and has been used in NASA. AMA if anyone here is curious about how the world around FM works.

jalcazar 5y ago

Program verification is an expensive activity. Navigating the cost-benefit trade-off of program verification is ultimately a business decision. https://t.co/IUCLtDLROC https://t.co/IUCLtDLROC

olivierduval 5y ago

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