I'd like to add belatedly that I think it's cool that you introduce the Curry-Howard stuff so early on, basically from the very beginning.