  Beloved Curry--Howard correspondence tells that types are intuitionistic
propositions, and in constructive math, a proof of proposition can be seen as
some kind of a construction, or witness, conveying the information of the
proposition. We demonstrate how useful this point of view is as the guiding
principle for developing dependently-typed programs.
