Getting a spec right is not the same as proving a theorem. It is the same as stating a theorem. And I absolutely disagree with you that making small pure programs magically makes them bugfree.