Michael Clarkson of "OCaml Programming: Correct + Efficient + Beautiful" [0] fame is currently publishing series of lectures "Software Foundations in Coq" [1] (

Michael Clarkson of "OCaml Programming: Correct + Efficient + Beautiful" [0] fame is currently publishing series of lectures "Software Foundations in Coq" [1] (new ones appearing once a week?) as a companion to [2] which looks as great as OCaml series. [0] https://www.youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b-I4XROIJhkIU https://www.youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b... [1] https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk... [2] https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.html https://clarksmr.github.io/sf-lectures/textbook/lf/Preface.h...