> It really should be "write software with a formal spec". The code is already a formal spec. Unless there are bugs in the language/compiler/interpreter, what

> It really should be "write software with a formal spec". The code is already a formal spec. Unless there are bugs in the language/compiler/interpreter, what the code is essentially formally well defined. As programming languages get better at enabling programmers to communicate intention as opposed to being a way to generate computer instructions, there's really no need for a separate "spec". Any so called "spec" that is not a programming language is likely not "formal" in the sense that the behavior is unambiguously well defined. Of course, you might be able to write the "spec" using a formal language that cannot be transformed into machine code, but assuming that the "spec" is actually well defined, then it's just that "compiling" the spec into machine code is too expensive in some way (eg. nobody has written a compiler, it's too computationally hard to deduce the actual intention even though it's well defined, etc.). But in essence it is still a "programming language", just one without a compiler/interpreter.