As noted by others the annotations would be active checks. More like proofs in coq than static text. That way you'd be building up a logical understanding of the code base that was machine verifiable sidestepping the issue of stale comments.
If done properly this could even feed into code dynamics to capture information on the runtime information. So that at every point in the program you could start asking questions like how many times did this line execute, what was the type of this variable at this point, how much memory was allocated, and so on and so forth.
