Also you can write a perfect specification get into implementation and have to step back and redesign.

Software is fast to iterate and test that a lot assumptions can be proven by actually writing the code.

Software is closer to gardening or painting. We discover a lot through practice and writing code. Then we can often write more formal specifications.

But formal method is impractical for most software upfront, and instead is likely used for more serious runtime failures or cost of life.

That's just my two cents.