Define what is a bug in a spec? I defined the program to do one thing and one thing only. What does does it mean when I have a bug in my definition? There's a definition for the definition? Makes no sense.
However, because we don't do proofs in software, there are bugs.