The way I personally see this happening is everything has to be formally verified. This will guarantee that the file written tomorrow will be successfully read by yesterday's programs, and that contemporary software is compatible with future OSes. (Does this mean that we freeze libc?) But there is a problem: there are a lot of quirks for hardware in modern OS/drivers, which add weird and possibly unreliable code. Does the hardware+firmware has to be formally verified too?
Do we have to run our software on all hardware that exists, e.g. starting from 6502 and until some future CPU?
Do we want to use POSIX? Subset of POSIX? cough Plan9? cough
Another problem I see is seemingly inevitable software bloating over time.
- What features do we have to include in our OS, our kernel?
- Does this list of features only grows over time?
- Do we want to have GUI as a requirement? What if UI paradigm changes?
There is also a bloating of protocols, e.g. TLS. Maybe replace TLS with CurveCP?
Related reading:
DOD Trusted Computer System Evaluation Criteria http://csrc.nist.gov/publications/history/dod85.pdf
Formally proven OS kernel: http://sel4.systems/
List of theorem proving systems on wikipedia: http://en.wikipedia.org/wiki/Category:Theorem_proving_softwa...
Note that Nqthm prover started in 1970. ACL2 has a HUGE collection of proofs for code https://github.com/acl2/acl2
Jonathan K. Millen, Security Kernel validation in practice (1976), "The correctness of a security kernel on a PDP-11/45 is being proved" DOI:10.1145/360051.360059 https://mega.co.nz/#!U8UAWLQY!YJ1YsOqe6E0jge5lGktBZiJUar1lu2...