It is also clear that you can write a formal spec down before writing down prose, if your language is simple and low-level enough.