To make this concrete: a couple times now in my career I've embarked on projects where setting up any level of formal verification at the beginning would have clearly been overkill, but where a few years later I really wished I had it for certain important pieces. And now since formal verification is so uncommon in my experience, I would have to play a lot of catch up to do it, even for a project that is clearly important enough for it even from the beginning. I think this is a pretty widespread experience.
This is intrinsic to the differing nature of the problems. Verifying the safety of a bridge design is computationally trivial, verifying the safety of non-trivial software is NP-Hard. Safety is so inexpensive to add in physical engineering designs that we invest a lot of effort removing incidental unnecessary safety.
While true, this depends very much on the design (or lack thereof) of the software system. Many of our software systems are more complex than necessary because they weren't designed or the designs weren't considered carefully enough. When the software is allowed to grow and accumulate masses of code virtually unchecked, it becomes computationally intractable to continue to verify the system.
Much of the software involved in aircraft, specifically, can be reduced to very simple designs and implementations where the necessary safety analysis is feasible.
The present complexity is often in the accumulation of legacy defects and corrections (fixing the right problem in the wrong place) or trying to fix hardware problems with software. I'm not 100% pro-rewrite, but many avionics software groups (that I've encountered) refuse any rewrites on certification grounds but end up with something unbearably complex as a result (simulating hardware databuses from the 1980s in software on a 1 GHz processor when the system was initially targetting a 16 MHz processor).
Yes, you can often do more complex design. Sometimes though it costs you centuries to choose a good combination of existing physical properties (architecture), and sometimes it's "just" decades (Gravity Probe B). Wanna propose similar approach to software? :)
The principles of flight don't change. The fundamentals of building a skyscraper or a bridge don't change. There are hundreds of years of learning behind those things that are still relevant today.
Building airplanes and bridges and skyscrapers is not hard at all. People do it all the time with a high success rate. The hardest part is scraping up the capital and managing the logistics. I'm sure none of that knowledge is required to get any kind of engineering certification.
If you redesigned every bridge and airplane from scratch, from first principles, you would have a tremendous failure rate no matter how many certifications you held. That's what software is - every project is a brand new thing that has never been done before - there isn't 200 years of learning to fall back on.
One of the worst things that could happen to the software industry is for bureaucrats and other people who know nothing about software to really believe it is an engineering discipline and try and regulate it as such. We'll all be forced to do a fantastic amount of busy work to meet arbitrary and archaic "engineering standards", and the software will actually decline in quality. You'll be fined $50,000 if you use tabs rather than spaces, or don't use yoda compares in your C. But as long as you are using spaces and yoda compares you won't be liable for a failure. Stuff basically like that.
Maybe when we have 200 years of experience writing software, rather than 50 or so, we can start to think about formalizing it as an engineering job.
Sorry but this is just gatekeeping bullshit. Most apps being built today by companies with the budget to build them are TODO apps, report apps, storefronts, big data mungers, CRMs, etc. They all just have different business requirements and domain specific knowledge. To think that every software project can't be categorized is ridiculous.
> all just have different business requirements and domain specific knowledge
Yeah - that's what I said. You realize that's where all the complexity is, right?
you're trying to create a barrier to standardization. You don't want to codify successful patterns to keep your job coveted.
>Yeah - that's what I said. You realize that's where all the complexity is, right?
That's not what you said.
Look, business processes are different at every single company. Especially between companies doing the exact same thing. Which means that the software ostensibly doing the exact same thing at each of these companies is going to vary dramatically. Because the software at a company aligns to the business processes of that company. This is the true heart of Conway's law: "organizations which design systems ... are constrained to produce designs which are copies of the communication structures of these organizations."
And there is no fixing this. It's baked directly into the axioms. If every company in a domain ran exactly the same way, there would be no such thing as a competitive advantage.
Ugh. I use as many libraries and services as possible so I can focus on writing code when no standard tools exist. That will keep me busy every day forever. If you think I'm out there sabotaging standardization efforts you're delusional. I wouldn't even know how to do that. Slash tires at a W3C convention or something?
and this is what company executives need to understand. Given the fleeting nature of software and the speed in which one can write working code (not strictly correct or bug-free, but something that apparently works) people are convinced that software development should be cheap -- or cheaper than say airplane design. Software design is thus seen as cost not investment and those flaws in specifying and writing correct core is then shown in not treated edge cases, sometimes catastrofically
I used to work at a large financial company who had an intensely rigorous approach to verifying it's software in both manual and automated ways, as well as a much more careful approach to writing code to begin with.
When I started here (a much smaller startup delivering marketing software for small business clients), I brought up that I was concerned about going to somewhere with a less comprehensive testing pipeline in place, to which I was told:
"It's not particularly important to be able to find bugs before they're released, it's more important to optimize the deployment speed so that we can release the fixes quickly"
Sounded crazy to me at the time, but I later realized it's really all about what your industry is optimizing for, and what would cost you more money.
Sure, those were not critical systems, they could be patched with minimal hasse to clients. However you can't really predict catastrophe costs. It could range from minor usability issues to hard to trace calculation errors that could jeopardise the whole production operation. If the company doesn't work work with prototypes it should invest heavily in test coverage, integration test and delivery pipelines
It's not only hard, but the cost/benefit (or the large penalties of catastrophic failure) works out so that it's worth it to go to that amount of effort. The same amount of effort doesn't go into building a backyard garden shed. I'll grant that we've gotten to the point where the cost/benefit analysis demands that we go to that amount of effort in critical situations.
We've generally made a decisive choice for functionality and cost over bugs.
Which isn't to say that I don't agree that there are areas: self-driving cars, airplanes (required here), human diagnostic software (already required here), etc that should have much tougher standards. But across the board ... I don't think people are willing to pay for that.
It's hard to make a safe building, and it's hard to make safe software. The difference is it's (often) incredibly obvious that a building isn't safe the moment you step into it. In software it's sometimes pretty much impossible to tell the difference between a stone temple and a house of cards.
Proper strong typing, not just the weak typing that is more common, provides these "danger detectors". It makes it a compile error. Compiler errors make things immediately obvious.
Type systems are very rich and most statically typed languages that are commonly used now can barely count as type systems when compared against what we know from mathematics and computer science. They merely describe the data format (or not in the case of nullable) and not acceptable inputs. They don't allow types for scenarios like requiring a function that exhibits these behaviors but not these other ones.
Pattern matching in combination with strong typing requires code that handles all possible inputs or you get a compiler error.
Dependent typing requires inputs to be within certain tolerances (not just adhering to a data format).
Type systems can also make certain race conditions impossible to create.
This is just not true. If anything, our "danger detectors" probably give off an equal amount of false positives and false negatives when judging the structural integrity of objects we're unfamiliar with. And the same holds true for code bases, which is exactly why it makes sense to hold software to a similar standard as physical engineering.
In software the mentality is that tests, or formal specs, or even thoughtful design, are luxuries. That it's better to just hire someone who can make the computer do things than spend twice as much on someone who can write "good" code and take twice as long to do so (whatever "good" means, because we have no standard). Of course for "the Uber for X" those standards may be fine. But for autonomous vehicles, or credit bureaus, or the nascent private space industry, they are absolutely not.