The Curry-Howard correspondence defines a relationship between programming languages and logical systems. Types correspond to propositions; programs correspond to proofs.
Iris is a logic designed for reasoning about the behavior of concurrent programs. So if we apply the Curry-Howard correspondence to Iris, we should be able to prove the behavior of programs... by writing more programs.
This project is an exploration of that idea.