A case study for reliable, reusable software

We describe our system Fred for extracting reliable and reusable programs from mathematical proofs via a variant of the Curry-Howard isomorphism. Our system extends the idea of extracting programs from formal mathematical proofs by the reuse of programs which have been guaranteed by the user. The rules for combining these two approaches are called the Curry-Howard protocol. We illustrate our system with a simple example based on warehouses holding spare parts.