As a musician, writer, and programmer, my experience has been that beautiful is harder than correct.

Correctness is possible to verify (not always easy, ofc). You simply throw out the incorrect programs and that's it.

Then, what's left is a bunch of correct programs, stating the same, in very many very different ways.

Now you need to choose one of them. They're all "correct" - they produce required results when given particular input - but they obviously are not 100% equivalent.

What do you use, then, to choose one implementation out of all the others?

I think to call that quality "beauty" is fine. And that striving for it in your own programs is also right. Requiring it from others is a tricky subject, but as long as you don't go there, there's nothing wrong with talking about the beauty of code, programs, solutions, and so on.

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): and it must run on top of an unreliable subsystem.

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.

All the way down to quantum mechanics, unfortunately.