Code is a formal specification. You can have layers of such specifications. The problem with viewing code as the specification is that a lot of languages obscure the intent and only reveal the how.
I'm working on a radio product, it's clear how data is being moved into certain buffers. It's clear when data is moved into certain buffers. It isn't clear why data is moved into certain buffers, or if the code is correct, only that it's being done.
A higher level specification set allows us to have a documented understanding of why the code does what it does, and allows us to reason about it at that level. It also makes it feasible to bring new people into the project, because 150k sloc (not a huge project, but not small) of largely low-level code is not something someone new can jump in on and understand quickly.
We also have something that's much easier to reason about when designing system tests, and to test the code against. We write the tests as though the specification were the reality, and test the code against that model to detect where it diverges. If we only had the code, what would we test it against? If it's its own spec, then it can't be wrong.
I'm working on a radio product, it's clear how data is being moved into certain buffers. It's clear when data is moved into certain buffers. It isn't clear why data is moved into certain buffers, or if the code is correct, only that it's being done.
A higher level specification set allows us to have a documented understanding of why the code does what it does, and allows us to reason about it at that level. It also makes it feasible to bring new people into the project, because 150k sloc (not a huge project, but not small) of largely low-level code is not something someone new can jump in on and understand quickly.
We also have something that's much easier to reason about when designing system tests, and to test the code against. We write the tests as though the specification were the reality, and test the code against that model to detect where it diverges. If we only had the code, what would we test it against? If it's its own spec, then it can't be wrong.