Doesn't the documentation have to then become as rigorous as code --- effectively a high-level language in its own right? So writing the documentation becomes, well, just like writing a program without testing it as you go, without benefit of tests or (if desired) static type checking. If so, then the development process turns the programmer into a kind of human compiler: translating the specs into a dialect of C for the safety-certified compiler.