You have good points, but I think you misunderstand the post in many ways. First, you do realize that there already has been an OS that has been formally verif

You have good points, but I think you misunderstand the post in many ways. First, you do realize that there already has been an OS that has been formally verified, right? It's called seL4. There is also a C compiler that has been formally verified. It's called CompCert. So there is a clear path to get there on the software side. Second, I am not referring to dynamic linking. Dynamic linking requires jump tables because the dynamic library will be mapped into a different spot for every process. That is not what I am suggesting. I am suggesting that the OS map the library into the same spot in every process. This means that no jump tables, and thus, the dynamic part of linking are required. Most importantly, the OS would not have to invoke the dynamic linker to execute the program. So what I am really suggesting is something like static linking, but with OS support for reducing binary code duplication. Think of it this way: say I had an OS that could take a static .a library and map it into memory. Then I compile my libc into a static library and tell the OS to map it at address 0x0A0000. Then when I compile programs, I tell the compiler that libc will be at address 0x0A0000. When running such a program, the OS recognizes that it needs libc at that address, so it maps it. Then it maps the program and just starts it. Of course, this would still require recompiling every program when libc changes, but if you keep the equivalent of LLVM IR around for every program, you only need to run the backend when that happens. As for pinning stuff to their own cores, it turns out that most transistors in a chip are not running all of the time. That would, in fact, be a problem because it would be too much power consumption and heat. The term for this is "dark silicon," by the way. So pinning stuff to their own cores and leaving those cores idle is not, in itself, a problem. The hope would be that the dark silicon would be balanced out by the fact that when the process gets a signal it needs to respond to, the OS does not need to do a process switch to start the process running again, which would save a lot of time. However, I could still be wrong about how well such a design would utilize cores. I acknowledge that. About the ring buffer, I would want hardware support for this, but if hardware support existed, then a process could try to read from the ring buffer. If there is no data, it could set a bit and go to sleep. Then when there is data, the hardware could wake up the process, and it could immediately start executing. Likewise for trying to write to a full buffer. Thus, instead of spinning on them, they would do something closer to how glibc uses futexes: check them and if no progress is possible, go to sleep, then wake up on a signal from the hardware. The double benefit from this design is that the OS would not need to get involved to wake processes up. However, I do acknowledge that the design includes things that don't even exist, even in a research paper. The blog post was sort of a target to hit eventually, in 30-50 years or so. Take it as a wish list, I guess.