Functional Pearl: Witness Me -- Constructive Arguments Must Be Guided with Concrete Witness

TL;DR

This paper explores how viewing proofs as witnesses in the Curry--Howard correspondence can guide the development of dependently-typed programs, emphasizing the constructive nature of proofs as concrete evidence.

Contribution

It introduces a perspective that uses witnesses to guide constructive proofs, enhancing dependently-typed programming practices.

Findings

Witness-guided proofs improve program correctness

Concrete witnesses facilitate constructive argument development

The approach aligns with Curry--Howard correspondence principles

Abstract

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.