Two serious concerns Formal reasoning about programs is viable! Two fundamental underpinnings Curry - Howard - Martin-Höf analogy Logical frameworks Proof checkers and theorem provers Higher order abstract syntax Some historical milestones Goal and scope of this course
