[learningstud]

Try programming in a proof assistant to see how inseparable computation and logic are. It gets more fundamental than the Curry-Howard correspondence when homotopy type theory enters the scene.