Comment by pizzafeelsright

> Pace makers, dialysis machines, brake lines.

That’s fair, including insulin pumps over Bluetooth with known vulnerabilities. Many vulnerabilities might be fixed or formally verified if they are part of the architecture.

> Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.

Both rely on inspections, routine maintenance, procedures, and fail-safe hardware afaik. Just like climbing gear.

Would formally verified software add anything? For example, could it cut the need for inspections or software maintenance? I think neither is going to change.

But what might change is that the specific spelling error on an elevator display is formally verified. It becomes about coziness with impressive amounts of paperwork that only a few people can understand.

Just changing one statement requires new verification, which is why formally verified code currently is not touched but ported verbatim into new projects and “rewrites”. That cost may decrease, which is nice but also not nice: the systems you currently want to formally verify are systems you might not want to alter without high friction in the first place.

I’m hopeful it will produce more robust software, and I’m by no means against it, but I’m skeptical of producing more when we might want to produce less.

> Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.

There's something called safety regulation. An installed elevator is very likely to have passed all the verification necessary for it to clear the safety bar. Same with the other devices you listed.

As for general code, it's mostly based on trust. But I see practices endorsed by the AI providers and trust is very low on my end.