Lambda the Ultimate

I had an old forum topic where I discussed a couple of ways that I thought we could solve the OS upgrade problem. I proposed a number of ways that I claimed would work around this problem, but all of my proposed solutions ended up being flawed in one way or another. I was pushing around a lump in the carpet.

The OS upgrade problem is how to build machines that allow provably correct self-upgrade. The goal is to allow the OS to install a new version of itself that could be exactly the same as the previous version or might have new additions or optimizations. My idea on how to do this has been to the OS and the lowest level exposed hardware abstraction and require the programmer to supply a proof that his new OS implementation conforms to the OS standard. The standard axioms should include all of the properties that you want every future OS to include, such as all operations terminating in an acceptable time, security requirements, etc.

The most powerful approach to this would be to show the soundness of the OS inside the language, since then you'd be able to show that an arbitrary upgrade is correct. But this would require also modeling the language implementation as part of the OS, which runs us into Godel's incompleteness theorems.

The practical solution in a logic with universes is to to start with 2^64 universe levels and go on with your life. Since each universe models the one below, you'd be able to model an OS with 2^64-1 levels on the first upgrade, 2^64-2 on the second, etc. Each time you upgrade your machine, you will only be able to prove the correctness of a logic with one fewer level, but in practice you'll never run out. This is kind of inelegant, though, so I wondered if we could do better.

I think I now see a way to do it that meets the requirement I imposed above - the OS upgrade should be able to implement itself without *any* change (even just the loss of a single universe out of 2^64). The idea is this: we axiomitize that a certain machine operation returns a number that is guaranteed to be a lower bound on the number of levels. There is a software operation that OS can use to decrease the number of levels (until it reaches zero). The current version of the OS can correctly prove that if it decreases the level count by one before passing control to the new OS, then the new OS will behave correctly (because it thinks there is one fewer level and we can prove that correct).

The trick is to give the user a way to increase the number of levels reported by the machine by pressing a button *in hardware* on the outside of the machine somewhere. When the user wants to upgrade his OS, he can only do it if he has enough levels. Upon running out, the button resets the universe count to 2^64 or whatever.

Taking the machine out of the loop on the level increase is the key to making this work. Any attempt to automate the process by teaching the OS how to press the button itself seems to require additional levels to avoid Godel.

This construction satisfies my goal of building machines that allow provably correct self-upgrade without any loss in consistency strength over time.