Yeah, in small examples it's pretty neat: Define a "sorted" property, write a law that checks that the list is sorted and contains the same elements and someone else implements the sort and together with a proof for correctness. However larger software systems have an exponentially larger surface for reasonable and unreasonable edge cases. When I hit ctrl+s in my editor I expect that my cursor does not change colour, that the window does not minimize, that the program does not crash if there is no disk space left and so on. I don't see how this does not devolve into "negative space programming" where the user would have to anticipate and constrain every possible unwanted behavior of his software.

That's an old "AI" joke. It went like that:

They asked a computer how to minimize production expenses at a factory. The computer said: "Do not manufacture anything, expenses will be zero".

I believe it's been around since expert systems at least.

Heh, it's like we all need to collectively read I, Robot yet again, and the myriad of SF books on the subjects. Black and white quickly dithers to grey.