tailcalled comments on The Plan

[tailcalled]

Proving program correctness seems closer to the MIRI approach to me.