We don't write formally verified code because writing the code to pass the verification is annoying and hard. If we're only writing the formally verified spec a

We don't write formally verified code because writing the code to pass the verification is annoying and hard. If we're only writing the formally verified spec and a program or AI generated the code, that's a bit easier, though it may have to get easier still before it becomes mainstream.