3 ms·

The only way out of this mess I see is throwing everything away and starting from scratch, using provably (machine verifiable proofs) correct software. I'm thi

• tsimionescu 6y ago
  If you started today, 50 years from now you may be able to run vim on such a system, but not sooner.
  • d3ckard 6y ago
    Original Unix was created in a couple of years. While your point has merit, you’re overestimating by much.
    • tsimionescu 6y ago
      Original Unix wasn't formally verified. seL4 took ~8 years from initial design to release (though apparently the verification was done after 3 years?), and it is a code base smaller than TypeScript. CompCert started in 2005 and it still can't compile all of C, and it doesn't go past the level of Gcc's -O1 optimizations. Formal verification is an extreme cost amplifier, and the cost is super-linear with the size of the code base. I don't think my estimate is unrealistic, depending on exactly what you would expect to have running before vi (I was assuming a complete OS including a kernel, device drivers, a C stdlib or equivalent, and a userspace similar to the GNU tools).