Avigad, one of the Lean authors has several resources cited elsewhere in Xena Project. These are really useful to learn the necessary background [1,2]. IMHO, l

Avigad, one of the Lean authors has several resources cited elsewhere in Xena Project. These are really useful to learn the necessary background [1,2]. IMHO, logic and type theory are the algebra and calculus of computer science. CS degrees should be designed around some core courses on these, in the same way Math degrees tend to build up on linear algebra and real analysis coursework. [1] http://avigad.github.io/logic_and_proof/ http://avigad.github.io/logic_and_proof/ [2] https://avigad.github.io/formal_methods_in_education/ https://avigad.github.io/formal_methods_in_education/