A user proposes using the latest language model with a massive token budget to create a complete open-source operating system based on the seL4 microkernel. The plan involves analyzing seL4, Genode, and Linux source code to adapt drivers and subsystems for an seL4-based environment.
- The model would analyze code from seL4, seL4_libs, sel4-tutorials, sel4test, and Genode repositories.
- It would gradually adapt selected Linux drivers for common hardware and add useful file systems.
- The process would be iterative, involving architecture proposals, compilation, testing, and error correction.
- The resulting system would be released as open source in compliance with existing licenses.
The post questions whether current models could complete significant parts of such a project if costs were not constrained and identifies potential obstacles like maintaining long-term plans or debugging on real hardware.