Reason about invariants and preconditions with ghosts of departed proofs.

Reason about invariants and preconditions with ghosts of departed proofs. The GDP library implements building blocks for creating and working with APIs that may carry intricate preconditions for proper use. As a library author, you can use gdp to encode your API's preconditions and invariants, so that they will be statically checked at compile-time. As a library user, you can use the gdp deduction rules to codify your proofs that you are using the library correctly.

gdp: Ghosts of Departed Proofs.