I think a real challenge with trying to work on specifications first is error handling -- you often find that a truly sound model is quite difficult to explain

I think a real challenge with trying to work on specifications first is error handling -- you often find that a truly sound model is quite difficult to explain to users. So some prototyping and iteration becomes necessary in my experience. Like, rustc only recently gained the ability to explain that the borrow checker rejected a program because a lifetime parameter was invariant. And this isn't even an artificial bit of complexity -- if you have mutability you are required to think about variance. If you have a Cell<&'static str> you cannot just turn that into a Cell<&'a str>, the way you can turn a regular &'static str into a &'a str. (Java programmers might be familiar with similar issues around ArrayList<Object>.)