May also sometimes, when designing algorithms, be useful for documenting pre- and post-conditions and invariants in procedural languages that lack embedding such specifications. You can't really reason about these things in the language itself and end up having to use something else (predicate calculus usually) but it's nice to at least have an indicator, as tfa suggests! What code doesn't do is important!
