The Coq system provides a simplified programming language for describing algorithms, the logical properties of those algorithms, and proofs that the logical properties are satisfied. The key feature of this language is a thorough version of typing as found in conventional programming languages. Although simplified, this language is powerful enough to describe advanced software, such as a Java virtual machine, a C compiler or a microprocessor.