2 ms·

I suspect ie didn't specify correct because correctness is impossible; with the following constraint (i'm surprised he didn't have as the last bullet point): an

• AnimalMuppet 7y ago
  On top of several unreliable subsystems. I think that's a big part of why it's so hard. You've got leaky, imperfectly understood, unreliable subsystems, and you're trying to build the best system you can on top of it. And what you produce inevitably is a leaky, imperfectly understood, unreliable system... which becomes somebody else's subsystem. And so it goes. You say: We need to create perfect subsystems! Formal verification (or robust type systems, or better requirements, or mathematical reasoning, or some other approach) will save us! But it's not that simple. It starts clear down at the hardware level. How much can you formally prove about your CPU? After taking into account it's errata sheet? The union of the errata sheets of all the revs of the CPU? If you're running on PCs, the errata sheets of every CPU that anybody could conceivably be running on? If you can't formally prove much about the CPU, how are you going to formally prove the OS and/or compiler? And if you can't formally prove those, how can you formally prove anything else? It's leaky, unreliable, incompletely understood subsystems all the way down.
  • dnautics 7y ago
    All the way down to quantum mechanics, unfortunately.