Software Documentation and Formality

An article linked via Slashdot about using documentation as a bug finding tool [1] gets me wondering about why documentation is so neglected. There are of course many, well researched and known reasons but a common theme I keep seeing is that documentation implies a degree of formality, ie: the necessity to describe something accurately.

This in addition with the fact that documentation tends to be very static and the antithesis of agile methods which concentrate on the code rather than the documents.

But maybe here is one issue that does need to be actively tackled and that is firstly, code is part of the documentation and secondly the documentation necessarily contains more than the code. Keeping these various aspects consistent is, of course hard - exceedingly so given that the underlying model that does link the various levels of description and abstraction together is never visible. The underlying model implies a formal definition of how documentation relates to code.

So far I've just managed to describe some of the ideas of the Model driven Architecture which apart from some academic work never really succeeded in solving the documentation-code issue. Probably the best example I've seen is the B-Method which does make the link between various descriptions of a system clear through formal refinement, albeit in the same language and with a very well-defined underlying model.

But what is it that we're really trying to convey using "documentation" - is it really an abstract description of the code, or better still an abstract description of what the system does, which then the code is a refinement of?

And at what level of abstraction?

[1] Documentation as a Bug-Finding Tool April 11, 2012 | Eric