The Curry-Howard correspondence is often brought up as a relation between proving and programming, but at least Martin-Löf actually attributes the connection to programming to Kolmogorov. Whereas today types are easily associated with programming, Martin-Löf presents the connection in the order Types-Proposition-Problems (whose "solutions" are programs), that's kinda surprising today. Read his seminal paper, Constructive mathematics and computer programming.

cs.tufts.edu/~nr/cs257/archive

I was looking into this after listening to a little story at the beginning of an ICFP19 talk by Wouter Swierstra, telling about Edsger W. Dijkstra telling about Martin-Löf telling about his type theory.

> He (Martin-Löf) was a very sympathetic speaker and convinced at least me (Dijkstra) that something (possibly even of great conceptual elegance) was going on. He spoke with an endearing care.

m.youtube.com/watch?v=iU7UtoM7

Dijkstra's notes (EWD879) that are quoted there are also a marvel in themselves. Like everything he ever wrote pretty much.

cs.utexas.edu/~EWD/transcripti

Show thread
Sign in to participate in the conversation
niu.moe

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !