“inject it into everyone”
I assume the resistence would be lesser if it didn’t involve syringes, and I doubt this is an unsolvable hard constraint, even though the scare factor seems load-bearing in your model.
Option is pervasive, ambient, environmental nanobot protection (together with 222nm light etc)
For real stability, the AI needs to be powerful enough that if one side tries to pull out of the deal and disable the AI surveillance on their side, they can’t. So the major powers need to trust the AIs enough to give them enough military power that the humans can no longer fight off the AIs, and the AIs are tasked with enforcing by force of arms that no one builds superintelligence or other terrible weapons and none of the major powers invade each other, at least until some condition is fulfilled
Plan A supposes mutually assured compute destruction, pldeging assets much like proof of stake, MAD all the way yo. (When thinking about it, feudal hostage exchange and marriage-based pacts are a kind of MAD as well).
I’m not sure what role the weaponized interdependence trend plays here.
overall, great post. Just noticed some apparent weak points and want to invite you to refine.
I like the direction of this post, having similar interests. However, I think the bubble metaphor is weaker than the rest of the argument, and that there are clearer ways to show why it makes sense to adopt formal methods.
Let’s start with the weakness of the bubble metaphor: you don’t go into the externalities, limitations, collaboration and upkeep needed to uphold and maintain a bubble. The world is becoming increasingly standardised, discrete, manageable; yet also increasingly convoluted, non-linear, surprising etc. Keeping up the standards sometimes works as if by magic (clock time seems just part of the territory nowadays). I’m lurking in a protocol research group that is looking into exactly things like this, and it is an interesting and tractable area, but also very messy!
For me, the argument is simpler: To get an AI to produce an artefact, that artefact needs to be specified. We have different ways to specify an artefact, from natural language, to unit testing, to linters, to e2e acceptance test, type-driven programming with algebraic invariants, to user feedback and testing. I’m surely missing some. These specifications can be seen as constraints in program-space, creating an intersection where variations of the produced artefact lives. The more constraints we have, the better. The “harder” our constraints are (as in not budging, not being flexible), the better. Formal specification is a way to make natural language harder, a better constraint. Nuff said :)
In my mind, the reason we don’t have pervasive property testing, algebraic laws, strongly typed systems, well-designed programming languages etc, is because adoption requires onboarding, which is costly. I hope ai will change the picture.