This piece is intended as an accessible intro; it talks about the beginnings of formal logic, how intuitionism in the debate on foundations of mathematics led to intuitionistic logic, and Gentzen's natural deduction.
It's from there that I found "Howard on Curry Howard", a published response to a letter Phil Wadler wrote to William A. Howard. It provides an excellent hint how Martin-Löf's work on dependent types was influenced by the Curry-Howard correspondence and natural deduction.
https://wadler.blogspot.com/2014/08/howard-on-curry-howard.h...
It seems the only other HN discussion about a post on natural deduction so far was this one: https://news.ycombinator.com/item?id=22324836
There is also one on Curry Howard: https://news.ycombinator.com/item?id=17748717
It's from there that I found "Howard on Curry Howard", a published response to a letter Phil Wadler wrote to William A. Howard. It provides an excellent hint how Martin-Löf's work on dependent types was influenced by the Curry-Howard correspondence and natural deduction. https://wadler.blogspot.com/2014/08/howard-on-curry-howard.h...