Computer-checked proofs can ensure properties of software.  Discussion of several aspects of this idea.