[adreid]

Yes, that is a large part of what I was saying.

Also, some things are so hard to specify formally that we still don't know have any kind of formal spec. Memory concurrency semantics is an example. It is only in the last couple of years that we got a good spec of fixed size memory accesses. Then Peter Sewell's group drops the bombshell that if you have mixed size memory accesses then you can't make programs sequentially consistent even if you add a memory barrier after every single memory access. But we still don't know how to formally specify the memory orderings associated with atomic accesses, instruction fetches, page table walks or device accesses. So, until then, we use the best natural language definition we can and hope we will be able to formalise it soon.

Also, there are parts of the natural language spec that I had not seen any value in... until I started worrying about whether the spec itself was correct or could possibly be shown to be correct. And now that I do worry about that, I am seeing new value in those parts.