Yes, long ago it was observed that the first step in proving software correct was a clear specification of what the software was supposed to do and that for a lot of realistic software writing that spec was unreasonably difficult.