Comment by pizzafeelsright
11 hours ago
This flows.
All of human knowledge, experience, distilled down to idempotent instructions and code for specific tasks, functions, situations is fully testable against a near infinite amount of fuzz and attacks.
We do not question the strength of steel if properly treated.
Code is no different. We will enter the point where code is finally trusted as a carabiner and rope for the life of a climber.
This doesn't follow. We've had code as trusted as that for _decades_. Common criteria and EAL was certified at the end of the 20th century. Before that there was the rainbow series in the US dating back to the 1980s [1].
It's absolutely cool to see this sort of validation process get cheaper and easier, but it means nothing if no one cares enough to do it. EAL1 certification can be as cheap as a beefy server, but it's not commonly done because effectively no one cares.
As microsoft learned with the zune just because it's cheaper or better at the same price doesn't mean anyone will use it. Culturally, we have to make the effort of verifying code worth it.
[1]: https://en.wikipedia.org/wiki/Rainbow_Series
Code needs to run on physical devices, which are prone to undervolting, bit flips, hardware bugs in specific batches, radiation, deterioration, and the like.
Preferably, I wouldn’t trust my life to a calculating device running on AA batteries while dangling from a rope.
Pace makers, dialysis machines, brake lines.
We also have fully redundant systems. The elevator for example required Otis to do this fantastic demonstration 150 years ago and now we don't think twice about it.
Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
> 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.
[flagged]
Oh here come the anthropic bot army.
Oh I wish I saw it!