I don’t think I understand what is meant by “a formal world model”.
For example, in the narrow context of “I want to have a screen on which I can see what python program is currently running on my machine”, I guess the formal world model should be able to detect if the model submits an action that exploits a zero-day that tampers with my ability to see what programs are running. Does that mean that the formal world model has to know all possible zero-days? Does that mean that the software and the hardware have to be formally verified? Are formally verified computers roughly as cheap as regular computers? If not, that would be a clear counter-argument to “Davidad agrees that this project would be one of humanity’s most significant science projects, but he believes it would still be less costly than the Large Hadron Collider.”
Or is the claim that it’s feasible to build a conservative world model that tells you “maybe a zero-day” very quickly once you start doing things not explicitly within a dumb world model?
I feel like this formally-verifiable computers claim is either a good counterexample to the main claims, or an example that would help me understand what the heck these people are talking about.
I don’t think I understand what is meant by “a formal world model”.
For example, in the narrow context of “I want to have a screen on which I can see what python program is currently running on my machine”, I guess the formal world model should be able to detect if the model submits an action that exploits a zero-day that tampers with my ability to see what programs are running. Does that mean that the formal world model has to know all possible zero-days? Does that mean that the software and the hardware have to be formally verified? Are formally verified computers roughly as cheap as regular computers? If not, that would be a clear counter-argument to “Davidad agrees that this project would be one of humanity’s most significant science projects, but he believes it would still be less costly than the Large Hadron Collider.”
Or is the claim that it’s feasible to build a conservative world model that tells you “maybe a zero-day” very quickly once you start doing things not explicitly within a dumb world model?
I feel like this formally-verifiable computers claim is either a good counterexample to the main claims, or an example that would help me understand what the heck these people are talking about.