So rather than trying to write down specifications for all that a program does I think it's much more productive to write down partial specifications. Perhaps multiple partial specifications. And then check them either by testing or by dynamic checks or by static checks. You never prove that your program is right. You just increase your confidence that it's right. And I think that's all that anybody ever does.
