Today's formal methods are proof and type systems.
As appetite, we give a very broad outline of interactive theorem proving and a perspective on software correctness of distributed systems.
As starter, we consider freely generated algebraic structures, such as (several varieties of) monoids: CM, PCM, ICM.
The main course of the talk is discussing the computational content of classical logic:
(A) We shortly consider simply-typed lambda calculus and its type system, relating it to minimal natural deduction.
(B) We extend lambda calculus with a control operator, relating it to classical natural deduction.
(C) We argue that sequent calculus formalizes certain implicit notions in natural deduction, and can be considered a meta-proof system.
(D) We relate the syntactical structure of sequents to the monoids we have seen as starter.
(E) We introduce focus, polarity, and generalized type connectives. We will see data and codata.
(F) We explain the mu-mu-calculus, relating it to classical sequent calculus.
(G) We argue that codata is related to object-orientated programming languages.
Dessert: plan, future work and curiosities such as kinds, dependent types, hypersequents.