> Curry-Howard executable version of the claim

I don't see how the code provided has any relation to the Curry-Howard correspondence, which is a statement relating types and proofs.