But all jokes aside, we're entering a new era where there's a paradox of pro-AI people going AI is really good, but not that good... when it kind of is that good.
We'll probably have ai monitors as a service, but the bulk of the safety should come from AI doing better job of reviewing tricky bugs since humans refuse to spend effort on writing more formal specifications.
Society's response to that was to build a new Net, walling off the rogue AIs of the Old Net behind the Blackwall and carrying on in a corporate hellscape.
I wonder if we'll see life imitating art on this one.
Code is formal specifications. It's just that programming language semantics has no domain related value of correctness. So you overflow an unsigned integer variable and got a lesser number which does violate addition rules. Or increase account A without decreasing account B, which violates accounting rules (and all kind of closed systems).
So it's up to the programmer to encode all of those rules. While we do have some tooling like type checking and memory safety, they are nowhere near enough. And encoding such thing in a language like Lean or TLA is brittle in terms of maintenance (which you do need to do as the real world evolves).
AI's spottiness is exactly what describes this era. AI can create amazing code/image/video/article exception XYZ really annoying qualities that somewhat hobbles its ability to be autonomously.
And sure, maybe those problems will go away once we're at month X of the madness but we're still at month Y so are going to going remain for some moment.
The bulk of the safety should come from AI doing better job of reviewing tricky bugs since humans refuse to spend effort on writing more formal specifications.
But that part is the key point. We've had many years of networks building inherently insecure structures with security tacked as feature and the primary security process being more ad-hoc stopgaps.
That the resulting code is many orders of magnitude larger and more complicated than the "informal" original, and often simply cannot exist, and is incomprehensible to most humans if it does, is left as an exercise for the reader.
I mean, formal methods cannot even prove collatz conjecture terminates. Somehow that thing seems to be running some sort of almost turing complete machine in the number encoding. Good luck formalizing existing software!