It's easier for software to have a catastrophic failure than a building, bridge, or dam. It's not really a fair comparison when those are like easy mode compared to software.
I don't think it's "easy mode" and more that they're just very different domains.
As time goes on, I feel more and more strongly that we shouldn't compare software engineering with other types of engineering at all. My younger brother works in the structural engineering space and the types of issues he's faced across different roles is very different to the types of issues I face in software.
Building design and construction have to handle the physical world and dealing with the realities of physically building the structure. Once it's built, however, the occupants don't make drastic changes to the building itself. In comparison, something like Facebook or Twitter needed to change drastically just to remain usable as they grew. "Just stop adding users" isn't a sensible solution to the problem.
Just to be clear that I do not excuse the, frankly, shit software design of Horizon and the fucking appalling behaviour of the Post Office throughout this scandal. I do think, however, that comparing software engineering the other types of engineering does a disservice to all and doesn't take us closer to actually improving the craft.
I've got ~15 years of software development under my belt. And I've also experienced a 2ish year stint where I was exposed to a lot of structural engineering.
The structural engineers take a piece of steel out into the desert and they dump sand on it until it collapses. Then they divide whatever weight the sand was by 3 and write it down into a book which is then published for all the other structural engineers. This type of steel with this type of configuration with this length can hold up to this much weight.
Meanwhile, in software engineering the limiting factor that prevents collapse is often "these sets of constraints and requirements are too complicated for the team to keep track of in their heads in this messy codebase". Not only do we not have a way to test this and publish the results, it's not even obvious what exactly you're even trying to measure.
[Cyclomatic complexity isn't very well correlated to defects (iirc lines of code is better correlated). Design patterns, best practices, and code smells are all just poetry that we use to story tell our ways out of blame. And Weyuker's 9 Properties are at best a waste of time. There is currently no way to measure bad code that fails under load until it does so in production.]
> There is currently no way to measure bad code that fails under load until it does so in production.
FWIW, techniques to perform such measures have existed for ~30 years in PL research (some of Rust's type system comes from this kind of research), but I don't know of any industrial code that makes use of it.
So far the only[] thing I've found was Weyuker's 9 Properties from measurement theory, and that did not seem particularly compelling.
Now, I get that linear/affine types and dependent types (and theorem provers, etc) can be used to prove that you're following the spec. But this doesn't prove that the code is easily comprehended by the people interacting with it. Code that is provably correct (even in the event where the spec is actually exactly what you want) can still fail because it's too complicated for anyone to modify it anymore.
For example, the function composition operator type in agda is kind of intimidating:
_∘_ : ∀ {a b c}
{A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
(∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
((x : A) → C (g x))
It looks like Camelot is just a variant of SML. I couldn't really find any information about Hobbes (at least, what I found is probably not what you're talking about).
Can you mention the features of these languages that you think are worth looking into?
Both of them use linear types and something kinda vaguely like Rust move semantics (and, in the case of Hobbes, time & space sandboxes) to guarantee statically that code will execute within given time and/or space bounds. I also wrote (~20 years ago) an extension of Erlang that could do something similar (for small subsets of Erlang).
Granted, this doesn't fulfill all the requirements for being resilient, but if we manage to make it usable (let's say as usable as Rust), it would be a pretty large step forward.
