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 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...