4 ms·
Random tangent: I was poking around your blog and found the entry "1985 Dijkstra interview"[1] and I was struck by this line: > The net effect of it seems to
by carapace 6y ago
Random tangent: I was poking around your blog and found the entry "1985 Dijkstra interview"[1] and I was struck by this line:
> The net effect of it seems to be that a full system for really acceptable programming will be at the same time a full system that will suffice for the description of constructive mathematics.
He said that in '85!? Wow.
[1] https://maniagnosis.crsr.net/2007/10/1985-dijkstra-interview.html https://maniagnosis.crsr.net/2007/10/1985-dijkstra-interview...
- a1369209993 6y ago> a full system for [knowably-non-buggy] programming will be at the same time a full system that will suffice for the description of constructive mathematics. That's basically the Curry-Howard correspondence[0], which was first explicitly stated in 1980. 0: https://en.wikipedia.org/wiki/Curry-Howard_correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence