I completed a MSc in Formal Methods a decade ago, and I've worked in software projects where the level of rigor was equivalent or superior to any classical engineering field. For example, railway signaling or some real time control systems. We handed in complex artifacts that have had zero defects throughout their lifetime (> 15 years).

I believe lightweight formal methods are quite promising and might let software move relatively quickly and economically while retaining some rigor. Look into Liquid Haskell for some ideas that might become mainstream.

Liquid Haskell looks similar to Eiffel in terms of contracts.

I imagine a whole bunch of power could be derived from this in Haskell. I don't know how heavily contracts were/are used in Eiffel (I don't think it's so popular these days).

It would be great to know if contracts had a measurably useful outcome on projects and what that measurable was (addressed a market that we otherwise wouldn't have been able to, dropped runtime errors to only system based errors, etc).

WRT your projects, I imagine it would be great to see your product out there working with a known level of uptime and quality. I could imagine it's a bit of a shift from the normal "throw it together" of ... a lot of software.

I'd be curious to know what it's like to work on day to day, year to year. I imagine lots of software will still be "throw it together" for a long time yet, but even if the subsystems are formally verified, it could have a useful impact on the software that consumes these (verified) modules.

Liquid Haskell is a bit different from Eiffel. On Eiffel, contracts were designed to be verified at runtime. There were some efforts to verify them at compile time, like Liquid Haskell does, but that's hard unless the whole language and type system are designed for that from the ground up.

As for my day to day job, I think the real difference with common software development was that requirements were very well understood right from the beginning. This allowed us to formalize them into axioms and then derive the implementation in a stepwise fashion using some Standard ML tooling.

I've also worked on proving theorems on existing software artifacts, but that's way harder both in terms of effort and number of defects.

I personally think it would be excellent if that was the only way you were allowed to code. Though I'd probably lose my job haha. I'd sleep better at night.

How does liquid haskell compare to typescript?

Obligatory joke: https://twitter.com/fireship_dev/status/1383835506664906756

The gp is arguing that companies should be held liable for the harm that they can and do cause. You are countering that argument by claiming that doing so would require all companies to adopt onerous measures. However, that counter argument is only valid if we assume that all companies can cause the same amount of harm and thus have equal liability, and that doing so is unavoidable.

That assumption is deeply flawed. We do not hold toy car manufacturers to the same standards as actual car manufacturers. We do not hold every manufacturer of screws to the same standards as the manufacturers of screws on airplanes. Or rather, we do hold them to the same standards, just we know that certain use cases basically can not cause too much harm in the event of failure and thus in practice the standards needed to mitigate the worst case are much lower.

Software liability does not mean that everybody suddenly needs to take the same care as safety-critical industries. It only means that if you are making safety-critical software and you are incapable of separating the safety of the critical components from the non-critical components. What it really means is the repudiation of the one-size-fits-all lowest common denominator expectation of quality.

Liability just means more controls to avoid blame and tighter specifications. Malpractice laws don’t make doctors less dangerous, they mostly encourage ass covering exercises.

I worked at a place that had a formally verified application running on some mainframe. It was wonderful, except that the process was excruciating and maintaining that validation prevented any changes. Every code change cost a minimum of $25,000 2002 dollars.

It was dumb. They would have been better off with a paper process and army of clerks.

how does linux fare in this scenario? few things are as critical in terms of infrastructure

I can imagine two possible scenarios for Linux (the kernel): companies either choose to double down on it as a collaborative venture in order to distribute the cost of verification, or it is abandoned in favour of vendors who provide verified kernels at tremendous expense but in hopes of locking their competition out of the market.

As for the rest of the open source ecosystem that goes into Linux (the operating system), it would probably be abandoned.

All the internet backbone routers, endpoint routers and switches, hardware firewalls, VPN concentrators, the SSH daemons, SSL software, RSA keyfobs and the like, the content delivery networks and DNS ecosystem, SSL public trust system, the connectivity providers from ISP networks and national and international fibre connections to cellular and wifi networks, web browsers which billions of people use to interact with untrusted content, (datacenters, AT&T Long Lines building style classic phone system, the postal service, electricity subsystems, food and water supplies...), even staying in tech you've basically got to exploit something else before you get to whatever underlying OS there is and even if you get to it there's not necessarily a need to attack it.

NotPetya which took down Maersk and did $300Mn of damages was apparently spread (through their Windows AD) by compromised admin accounts which they were lax at managing[1] rather than kernel exploits. The SolarWinds Orion security flaws were blamed on weak passwords, not OS kernel exploits. And if getting inside, something like last month's SystemD/polkit exploit[2] shows that attacking the kernel isn't always necessary for privilege escalation.

Linux the kernel is important but it's the heart inside the ribcage, not the first or last line of defense, or the main thing to target.

[1] https://gvnshtn.com/maersk-me-notpetya/

[2] https://github.blog/2021-06-10-privilege-escalation-polkit-r...

The point is that if legislation were introduced that resulted in liability it would likely completely decapitate the FOSS ecosystem (among other things).

Why would it? If faced with the choice of taking liability for using Linux or rebuilding Amazon shop + AWS + Kindle + Echo on Windows I'd guess Amazon would do the former, wouldn't you?

In the short term? Perhaps. They might just develop their own proprietary OS - they already design custom CPUs!

I imagine it would depend heavily on how large the liability was. I expect individual components would begin being replaced with "certified" commercial alternatives. If not existing ones, definitely new ones. Remember that they make money by selling to customers who would also be subject to the same rules. Look at healthcare, aviation, and finance for concrete examples of the effects (both negative and positive) that red tape has on software and IT policies.

There's an entire FOSS ecosystem and the vast majority of it is composed of small-ish slow moving projects. The tech industry is also an entire ecosystem full of small and medium sized players. Even if behemoths such as mainline Linux and AWS somehow survived unchanged I would expect a much greater chilling effect on smaller players that couldn't afford to take on such risks. New companies and software projects would become very difficult to get off the ground (healthcare is a good example here). With few to no new entrants forward progress would slow to an absolute crawl.

All of this has downstream effects. Fewer consumer devices running Linux would mean even less hardware support. Security related liabilities would almost certainly mean more vendor locked hardware. Would companies like Purism remain viable (or even legal)? The steady stream of new FOSS users and contributors would almost certainly dwindle.

Depending on how such regulation was written, could open source contributors themselves become liable for a freely provided product?

Actually it's simpler. People and organizations would just move to a jurisdiction where such liability laws didn't exist. Apple would move. Microsoft would move. Google would move.

And then the US would be forced to decide whether to accept imports of foreign devices and software (created under the no-liability framework) or to stay with homegrown technology frozen in time.

The best thing you can say about this proposed reform is that it would make a great plot for a sci-fi novel.

Tech companies can't even manage to leave San Francisco's outrageous cost of living and rising crime, much less the United States.

You think they are trying? When VC and executives live in walled castles and own multiple rental and investment property?

I mean the hub thing and synergistic collaboration are cool but employees are not 3x more productive because of it.

> or to stay with homegrown technology frozen in time.

Why would it be frozen in time?

> Why would it be frozen in time?

Local development would rendered unable to compete with the fast moving zero-liability model that quickly and cheaply delivered the features that consumers wanted. Either it's import would be banned or the local industry would crumble.

I don't completely disagree but

> you get paid a lot less

Isn't that the point? That is, the argument is right now the money goes to the devs, management, and stockholders, when it rightfully should go to those people damaged by the software (or toward preventing them from being damaged).

> the companies and industries move very slowly

How much of this is due to liability law and how much is due to natural aspects of the relevant technology? Liability law may be part of the reason, but software probably naturally moves faster than other engineering fields.

> Isn't that the point?

If the money is supposed to go towards people preventing damage, wouldn't that include devs?

> How much of this is due to liability law and how much is due to natural aspects of the relevant technology?

I can only speak from my own experience in biotech, but moving slowly was due to a lot of compliance box-ticking that didn't actually contribute a lot to either safety, reducing defect rate or meeting requirements. Conway's law applied: since bio engineers and lab techs move slowly, so did the software org.

> fields where the companies are liable for bad stuff...

> * the companies and industries move very slowly

The reason the rest of us move so fast is we skip safety, security, quality, and maintainability to get to market. Those things are usually perceived "not bringing immediate customer value".

> The reason the rest of us move so fast is we skip safety, security, quality, and maintainability to get to market.

And deliver cheaper results.

And still, the Toyota breaking microcontroller code showed that coding practices in Real Engineering are somehow even worse. I hope that improved since then.

> What we do in software is not real engineering, not even close.

The only reason our processes and practices aren't much heavier is because the stakes are lower. People do not die if a Tweet doesn't make it through, but they do if a bridge collapses through.

The threat model is also significantly different. If we go back to the bridge analogy, a company like Microsoft has to deal with tens of thousands of people trying to blow it up or find some weakness every day, while a million people are going over it. Just by sheer laws of scale they are going to have a tougher time, Real Engineering or not.

> People do not die if a Tweet doesn't make it through

True, and what you're saying is generally true. But what were the total consequences of the Equifax breach? We can't even quantify it. Snowden himself in the article mentions activists and journalists being killed because of these vulnerabilities. There are definitely counterexamples.

That's true. I suspect part of the problem there is lack of liability and therefore lack of willingness to pay for security. They're just going to lose the best security engineers to Google and Microsoft.

That is due to issues with how Equifax operated (and related lack of meaningful consequences). It has nothing to do with a lack of liability for software companies.

Is moving more slowly in software a bad thing? I can just imagine an alternative world where people are better off, using sites that look like HN but are secure and work in their best interest.

There would be no sites. There would be no web.

>I mean like Real Engineering fields. What we do in software is not real engineering, not even close. That has pros and cons.

"Real Engineering" has definition and it fits SE, doesn't it?

Computer industry iterated and managed to reach the point where we can move really fast and do not break computers with bad code. That's result of thousands of hours of engineering effort of previous generations.

>Engineering is the use of scientific principles to design and build machines, structures, and other items, including bridges, tunnels, roads, vehicles, and buildings. The discipline of engineering encompasses a broad range of more specialized fields of engineering, each with a more specific emphasis on particular areas of applied mathematics, applied science, and types of application. See glossary of engineering.

How about hardware engineers or software engineers working on hardware? I figured it achieves a certain middle ground. You are still writing code but you get to touch real things and may burn yourself if you work closely with the hardware, plus you need to pay more attention to security.

> I saw someone else talking about Rust, but I don't think that's what would happen in such a world.

I agree.

Let's not use tools as a crutch. Roman engineers built bridges that are still standing today with little to no maintenance. There's no indication that those structures are going to fail anytime soon either. I think we can agree that their tooling was worse than our current bridge building tools.

> I mean like Real Engineering fields. What we do in software is not real engineering, not even close. That has pros and cons.

So the word engineer is probably loaded if not dated, a throwback to engineering's boom in the 19th and early 20th century. No idea why we still use it since software is more like math than anything else. Computer scientist just never stuck.

> Roman engineers built bridges that are still standing today

Roman engineers didn't understand the principles of civil engineering; I'm sure they built a lot of stuff that fell down (survivorship bias). So they started massively over-engineering their structures ("moar rocks!")

> I'm sure they built a lot of stuff that fell down

Survivorship bias is the favourite catchphrase for HN these last few years.

I think you overestimate the importance of academic theory over practicality.

"Moar rocks" is a perfectly reasonable way ro fortify a structure. Because 1000 years from now engineers will be wondering how any of our stuff survived ("moar cement and steel rods!")

So yeah, I have a healthy respect for practicality.

Sounds more like Ada than Rust.

So called "Real Engineering" fields kill people at such a high rate. Software engineers are way better. Despite all the value created, a vanishingly small number of people have been killed.

That's the funny thing. As a software engineer, if I have to build something that might kill someone, I just don't do it. But so-called "real engineers"? Bam, condo building down, people dead. Bridge down, people dead. Tacoma Narrows? Experimenting on people.

If "real engineers" were half as good at their job as I am at mine, we'd have a space elevator and people would be going up and down it every hour and the only problem they'd face is that the music is sometimes not that great. But they're too busy killing people to create $10 in value. I'm too busy not killing people and creating $1 million in value. The numbers don't lie, dude. The numbers don't lie. More value made. Fewer dead people.

People don't like to hear it because of the fetishization of this "Real Engineering" nonsense. But it's true. Software engineering's generational scandals are outdone by a "real engineering" project every day.

Maybe it's because real engineering has higher stakes than a crud app. Condos can kill, bridges can kill, Javascript forms or video game engines generally can't. If they could we'd witness a lot more deaths, despite your confidence.

I have a personal philosophy: "if you can't do it well, don't do it at all". That's because I prize my ability at what I do. I am good at it. I am a craftsman. Not like these fly-by-night characters busy dropping concrete on people's heads. Maybe I need to teach these "real engineers" something about building things haha: "If you can't do it without killing people, don't do it". Man, that's a motto for the ages. You'd think you don't have to teach people that, but here we are.

Maybe we should teach them ethics, because whatever class they took on that, it didn't take. As a practitioner of quality and making money with zero killing, I could help.

>I have a personal philosophy: "if you can't do it well, don't do it at all". That's because I prize my ability at what I do. I am good at it. Maybe I need to teach these "real engineers" something about building things haha: "If you can't do it without killing people, don't do it". Man, that's a motto for the ages. You'd think you don't have to teach people that, but here we are.

You're trying too hard. It's embarrassing.

Why bother with the software engineering, your moral sensibilities are needed everywhere. It's not every day someone emerges capable of writing a todo app in react without killing anyone

HAHA! What can I say? Some of us are made of sterner stuff.

I see an awful lot of skyscrapers not falling down every day, stands to reason some engineers are good at what they do, no?

Oh there are good engineers, certainly. But the field as a whole clearly is immature since it causes more deaths than software engineers do.

I actually agree with you. People keep doing shitty jobs in real engineering e.g. construction. It's just most of the time people don't have the skills to notice it.