It is nice to see CBPV on HN. It is a calculus that deal with a fundamental choice in PL of how to approach evaluation. For a different take, here is the first part of a mini series of posts on CBPV that aims at working out the connection to logic ("polarised natural deduction"): https://burakemir.ch/post/cbpv-pt1-small-steps/