This is such a great and actually important comment. I’ve been obsessed with program correctness / verification for a while now. It just seems like the holy gra

This is such a great and actually important comment. I’ve been obsessed with program correctness / verification for a while now. It just seems like the holy grail that we can’t fully attain yet. But you keep bumping into certain walls, and the fact that correctness can only be relative to a given specification is a profoundly huge wall. There’s no checking to see if your specification is under-specified.