I did some of this stuff in college and what bugged me was that the spec actually ended up more complex than the code and it had bugs.

That was a long time ago and they said that formal methods were the future back then, too.

It's possible for that to happen but probably means either the function is too trivial or you're missing some abstraction in the spec