But if it's easier to write the specification than the code, that must mean that the programming language isn't very good. And yes! This is borne out by the sort of programming errors that are found when comparing the specification to the implementation:
These are mostly solved by using a decent programming language such as Python.
- Buffer overflows
- Null pointer dereferences
- Pointer errors in general
- Memory leaks
- Arithmetic overflows and exceptions
Ben Laurie talks about this in his post on formal methods.