In this episode I speak with Paul Chiusano (@pchiusano), creator of Unison, about his ambitious vision for the future, where we can abstract over distributed computing, and there are no apps.

In this episode I speak with Paul Chiusano (<a class="ProfileHeaderCard-screennameLink u-linkComplex js-nav" href="https://twitter.com/pchiusano">@pchiusano</a>), creator of <a href="unisonweb.org">Unison</a>, about his ambitious vision for the future, where we can abstract over distributed computing, and there are no apps.

Playful explorations of the rich past and exciting future that we're all building with our silly little computers. Hosted by Jimmy Miller and Ivan Reese.

Playful explorations of the rich past and exciting future that we're all building with our silly little computers. Hosted by Jimmy Miller and Ivan Reese.

Future of Coding

Unison's Paul Chiusano on how Abstraction Will Save Distributed Computing

Dave Ackley's paper Beyond Efficiency is three pages long. With just these three pages, he mounts a compelling argument against the conventional way we engineer software. Instead of inflexibly insisting upon correctness, maybe allow a lil slop? Instead of chasing peak performance with cache and clever tricks, maybe measure many times before you cut. So in this episode, we're putting every CEO in the guillotine… (oh, that stands for "correctness and efficiency only", don't put us on a list)… and considering when, where, and how to do the robust thing.

Links

$ patreon.com/futureofcoding — The most recent bonus episode is a discussion with Stefan Lesser about new "laws of physics" we can invent inside the computer.

Don't destroy the earth, then make sure your thing can't be destroyed, then don't destroy your data, and finally, do your damn job, AAAAAAAAAAAAAAAAAAAAAAAAAAA.
A Software Epiphany, and the accompanying HN discussion — giga viral, so sick
PartyKit? Nice!
What started as a simple todo list turned into an ocean of tech boy milk and, ultimately, the AI apocalypse.
Jepsen is a rough, rugged, deeply thoughtful and fantastically cool approach to distributed systems testing, by Kyle Kingsbury. Also, we didn't talk about it, but his reversing / hexing / typing / rewriting / unifying technical interview series is essential reading.
Ivan's examples of robustness vs efficiency were RAID, the CAP theorem, Automerge, the engineering of FoundationDB, and Byzantine fault tolerance— all of which stake out interesting territory in the efficiency/robustness tradeoff spectrum, all of which are about distributed systems.
Can programming be liberated from the von Neumann style?, a paper by John Backus.
We Don't Really Know How to Compute!, a talk by Gerald Sussman.
The Robust-First Computing Creed is rock solid.
The Wikipedia article on von Neumann architecture did not come through with the goods.
Ivan works with Alex Warth now, and thus may fairly speak in half-truths like "I've been working with constraints recently…"
The Demon Hoard Sort
Bogosort is never coming to Dreamberd
The Witness was made by Jonathan Blow, who has Aphantasia, but he also made a game called Braid, and Braid is good.
Datamosh is a creative misuse of the lack of robustness that comes from storing diffs instead of full state snapshots. Here's a lovely gallery of examples.
Abstraction by xkcd
Reverse Engineering the source code of the BioNTech/Pfizer SARS-CoV-2 Vaccine
Can't let Lu get through the above without derailing onto Fiverr, PCP, Fight Club, and the Dust Brothers.
Randy Newman was nearly quoted in Ackley's Indefinite Scalability for Living Computation — god help you if you read our show notes and don't listen to the episode.
"It is difficult", says Upton Sinclair when asked about Jimmy Miller being Jimmy Miller, and how we all ought to approach our own sense of Jimmy Miller.

Music featured in this episode:
Hawker News by user: spiralganglion
Corporate World by the Dust Brothers

No more jokes! Find us at these normal places:
Ivan: Mastodon • Website
Jimmy: Mastodon • Website
Lu: Mastodon • Website
Dave: Mastodon • Website

Send us email, share your ideas in our Slack, and support the show on Patreon. Yes, do all three please.

<a href="https://www.cs.unm.edu/~ackley/">Dave Ackley</a>'s paper <a href="https://www.cs.unm.edu/~ackley/be-201301131528.pdf">Beyond Efficiency</a> is three pages long. With just these three pages, he mounts a compelling argument against the conventional way we engineer software. Instead of inflexibly insisting upon correctness, maybe allow a lil slop? Instead of chasing peak performance with cache and clever tricks, maybe measure many times before you cut. So in this episode, we're putting every CEO in the guillotine… (oh, that stands for "correctness and efficiency only", don't put us on a list)… and considering when, where, and how to do the robust thing.
Links
$ <a href="https://www.patreon.com/futureofcoding">patreon.com/futureofcoding</a> — The most recent bonus episode is a discussion with Stefan Lesser about new "laws of physics" we can invent inside the computer.
Don't destroy the earth, then make sure your thing can't be destroyed, then don't destroy your data, and finally, do your damn job, AAAAAAAAAAAAAAAAAAAAAAAAAAA.
<ul>
<li><a href="https://johnwhiles.com/posts/programming-as-theory">A Software Epiphany</a>, and the accompanying <a href="https://news.ycombinator.com/item?id=38324486">HN discussion</a> — giga viral, so sick</li>
<li><a href="https://www.partykit.io/">PartyKit</a>? Nice!</li>
<li>What started as a <a href="https://mastodon.social/@TodePond@mas.to/111402970410628418">simple todo list</a> turned into an <a href="https://twitter.com/tldraw/status/1724892287304646868">ocean of tech boy milk</a> and, ultimately, the <a href="https://news.ycombinator.com/item?id=38309611">AI apocalypse</a>.</li>
<li><a href="https://jepsen.io/">Jepsen</a> is a rough, rugged, deeply thoughtful and fantastically cool approach to distributed systems testing, by <a href="https://aphyr.com/">Kyle Kingsbury</a>. Also, we didn't talk about it, but his <a href="https://aphyr.com/posts/340-reversing-the-technical-interview">reversing</a> / <a href="https://aphyr.com/posts/341-hexing-the-technical-interview">hexing</a> / <a href="https://aphyr.com/posts/342-typing-the-technical-interview">typing</a> / <a href="https://aphyr.com/posts/353-rewriting-the-technical-interview">rewriting</a> / <a href="https://aphyr.com/posts/354-unifying-the-technical-interview">unifying</a> technical interview series is essential reading.</li>
<li>Ivan's examples of robustness vs efficiency were <a href="https://en.wikipedia.org/wiki/RAID">RAID</a>, the <a href="https://en.wikipedia.org/wiki/CAP_theorem">CAP theorem</a>, <a href="https://automerge.org/">Automerge</a>, <a href="https://www.youtube.com/watch?v=4fFDFbi3toc">the engineering of FoundationDB</a>, and <a href="https://en.wikipedia.org/wiki/Byzantine_fault">Byzantine fault tolerance</a>— all of which stake out interesting territory in the efficiency/robustness tradeoff spectrum, all of which are about distributed systems.</li>
<li><a href="https://dl.acm.org/doi/10.1145/359576.359579">Can programming be liberated from the von Neumann style?</a>, a paper by <a href="https://en.wikipedia.org/wiki/John_Backus">John Backus</a>.</li>
<li><a href="https://www.youtube.com/watch?v=HB5TrK7A4pI">We Don't Really Know How to Compute!</a>, a talk by <a href="https://en.wikipedia.org/wiki/Gerald_Jay_Sussman">Gerald Sussman</a>.</li>
<li>The <a href="https://andrewwalpole.com/blog/an-introduction-to-robust-first-computation/">Robust-First Computing Creed</a> is rock solid.</li>
<li>The Wikipedia article on <a href="https://en.wikipedia.org/wiki/Von_Neumann_architecture">von Neumann architecture</a> did not come through with the goods.</li>
<li>Ivan works with <a href="https://alexwarth.github.io/">Alex Warth</a> now, and thus may fairly speak in half-truths like "I've been working with constraints recently…"</li>
<li>The <a href="https://www.youtube.com/watch?v=helScS3coAE">Demon Hoard Sort</a></li>
<li><a href="https://en.wikipedia.org/wiki/Bogosort">Bogosort</a> is never coming to <a href="https://github.com/TodePond/DreamBerd">Dreamberd</a></li>
<li><a href="https://en.wikipedia.org/wiki/The_Witness_(2016_video_game)">The Witness</a> was made by <a href="https://en.wikipedia.org/wiki/Jonathan_Blow">Jonathan Blow</a>, who has <a href="https://en.wikipedia.org/wiki/Aphantasia">Aphantasia</a>, but he also made a game called <a href="https://en.wikipedia.org/wiki/Braid_(video_game)">Braid</a>, and Braid is good.</li>
<li><a href="https://en.wikipedia.org/wiki/Compression_artifact#Artistic_use">Datamosh</a> is a creative misuse of the lack of robustness that comes from storing diffs instead of full state snapshots. Here's a <a href="https://eyecannndy.com/technique/glitch#datamosh">lovely gallery</a> of examples.</li>
<li><a href="https://xkcd.com/676/">Abstraction</a> by xkcd</li>
<li><a href="https://berthub.eu/articles/posts/reverse-engineering-source-code-of-the-biontech-pfizer-vaccine/">Reverse Engineering the source code of the BioNTech/Pfizer SARS-CoV-2 Vaccine</a></li>
<li>Can't let Lu get through the above without derailing onto <a href="https://en.wikipedia.org/wiki/Fiverr">Fiverr</a>, <a href="https://en.wikipedia.org/wiki/Phencyclidine">PCP</a>, <a href="https://en.wikipedia.org/wiki/Fight_Club">Fight Club</a>, and the <a href="https://en.wikipedia.org/wiki/Dust_Brothers">Dust Brothers</a>.</li>
<li><a href="https://en.wikipedia.org/wiki/Randy_Newman">Randy Newman</a> was nearly quoted in Ackley's <a href="https://cdn.aaai.org/ojs/9802/9802-13-13330-1-2-20201228.pdf">Indefinite Scalability for Living Computation</a> — god help you if you read our show notes and don't listen to the episode.</li>
<li><a href="https://www.goodreads.com/quotes/21810-it-is-difficult-to-get-a-man-to-understand-something">"It is difficult"</a>, says <a href="https://en.wikipedia.org/wiki/Upton_Sinclair">Upton Sinclair</a> when asked about Jimmy Miller being Jimmy Miller, and how we all ought to approach our own sense of Jimmy Miller.</li>
</ul>
Music featured in this episode:
<ul>
<li><a href="https://ivanish.ca/hawker-news">Hawker News</a> by <a href="https://news.ycombinator.com/user?id=spiralganglion">user: spiralganglion</a></li>
<li><a href="https://www.youtube.com/watch?v=dAtX4PjUXrM">Corporate World</a> by the <a href="https://en.wikipedia.org/wiki/Dust_Brothers">Dust Brothers</a></li>
</ul>
No more jokes! Find us at these normal places:
<ul>
<li>Ivan: <a href="https://mastodon.social/@spiralganglion">Mastodon</a> • <a href="https://ivanish.ca/">Website</a></li>
<li>Jimmy: <a href="https://hachyderm.io/@jimmyhmiller">Mastodon</a> • <a href="https://jimmyhmiller.github.io/">Website</a></li>
<li>Lu: <a href="https://mas.to/@TodePond">Mastodon</a> • <a href="https://www.todepond.com/">Website</a></li>
<li>Dave: <a href="https://hachyderm.io/@livcomp">Mastodon</a> • <a href="https://www.cs.unm.edu/~ackley/">Website</a></li>
</ul>
Send us <a href="mailto:admin@futureofcoding.org?subject=Email%20from%20a%20listener">email</a>, share your ideas in our <a href="https://futureofcoding.org/community">Slack</a>, and support the show on <a href="http://patreon.com/futureofcoding">Patreon</a>. Yes, do all three please.

Beyond Efficiency by Dave Ackley

In the spirit of clearly communicating what you're signing up for, this podcast episode is nearly three hours long, and among other things it contains a discussion of a paper by author Mary Shaw titled Myths & Mythconceptions which takes as an organizing principle a collection of myths that are widely believed by programmers, largely unacknowledged, which shape our views on the nature of programming as an activity and the needs of programmers as people and the sort of work that we do as a sort of work, and where by acknowledging these myths the three of us (Mary Shaw primarily, and by extension Jimmy and I, those three people, that's it, no other people appear on this podcast) are able to more vividly grip the image of programming with our mind's eye (or somesuch) and conceive of a different formulation for programming, and in addition to these myths this paper also incudes a number of excellent lists that I take great pleasure in reading, beyond which I should also note that the paper does a job of explaining itself and that hopefully you'll find I've done a similar job, that's the spirit, please enjoy.

Links

$ patreon.com/futureofcoding — I've recently changed it so that there's only 1 instance of the INTERCAL tier available, so if you're interested in those perks you'd better hop on it quick before nobody else does!
There's also a video, though I haven't watched it.
Claude Shannon would have something to say about revealing information.
Top 10 Hits of the End of the World is an album by Prince Rama. Listen to it as loudly as you can on Bandcamp, Spotify, or Apple Music.
Val Town is the new startup by Future of Coding community founder Steve Krouse
Ivan recently took a job at Ink & Switch on the "Ink" research track.
Programmer Bums, or, rather, Computer Bums
Limmy's Wa
Retool
MythBusters
The Flop House's Final Judgements: Good-Bad, Bad-Bad, Kinda-Like
CRDT
Data
Robust-First Computing is an approach championed by the hero Dave Ackley, and I have a well-informed hunch that you'll be hearing a lot more about it in future episodes.
The T2 Tile Project is another Ackley joint that, perhaps, works as a wild example of what Mary Shaw means when she talks about an "execution ecosystem".
Devine's talk at Strange Loop: An approach to computing and sustainability inspired from permaculture
MUMPS (the medical thing, not to be confused with mumps the medical thing) is used by Epic (the software company, not to be confused with Epic the software company).
The Glass Cannon podcast network.
Lu's SPLASH talk Cellpond: Spatial Programming without Escape
The Turing tarpit
Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire by Erik Meijer, Maarten Fokkinga, Ross Paterson.
Richard D. James is the same person as Richard P. (Peter) Gabriel, right?
Similarly, see Neil Armstrong's work on Erlang (which is popular in telephony, right?).
The Witness is not going to appear in our show notes.
Jack Rusher. Jack Rusher? Jack Rusher!
TrainJam
Gary Bernhardt's talk Ideology

Nobody remarked on these silly links last time, so this time I'm drawing more attention to them:
Tode: Neopets • MySpace
Berd: Angelfire • Orkut
Bot: Geocities • Friendster

https://futureofcoding.org/episodes/069

In the spirit of clearly communicating what you're signing up for, this podcast episode is nearly three hours long, and among other things it contains a discussion of a paper by author Mary Shaw titled <a href="https://dl.acm.org/doi/pdf/10.1145/3480947">Myths &amp; Mythconceptions</a> which takes as an organizing principle a collection of myths that are widely believed by programmers, largely unacknowledged, which shape our views on the nature of programming as an activity and the needs of programmers as people and the sort of work that we do as a sort of work, and where by acknowledging these myths the three of us (Mary Shaw primarily, and by extension Jimmy and I, those three people, that's it, no other people appear on this podcast) are able to more vividly grip the image of programming with our mind's eye (or <a href="https://aphantasia.com/">somesuch</a>) and conceive of a different formulation for programming, and in addition to these myths this paper also incudes a number of excellent lists that I take great pleasure in reading, beyond which I should also note that the paper does a job of explaining itself and that hopefully you'll find I've done a similar job, that's the spirit, please enjoy.
Links
$ <a href="https://www.patreon.com/futureofcoding">patreon.com/futureofcoding</a> — I've recently changed it so that there's only 1 instance of the INTERCAL tier available, so if you're interested in those perks you'd better hop on it quick before nobody else does!
<ul>
<li>There's also a <a href="https://www.pldi21.org/prerecorded_hopl.K1.html">video</a>, though I haven't watched it.</li>
<li><a href="https://en.wikipedia.org/wiki/Claude_Shannon">Claude Shannon</a> would have something to say about revealing information.</li>
<li><a href="https://en.wikipedia.org/wiki/Top_10_Hits_of_the_End_of_the_World">Top 10 Hits of the End of the World</a> is an album by Prince Rama. Listen to it as loudly as you can on <a href="https://princerama.bandcamp.com/album/top-ten-hits-of-the-end-of-the-world">Bandcamp</a>, <a href="https://open.spotify.com/album/2pbvIz40L97L87KGFnFnme?si=zbzT8JHKTCGJkObmh4qN1g">Spotify</a>, or <a href="https://music.apple.com/ca/album/top-ten-hits-of-the-end-of-the-world/1583505277">Apple Music</a>.</li>
<li><a href="https://www.val.town/">Val Town</a> is the new startup by Future of Coding community founder <a href="https://stevekrouse.com/">Steve Krouse</a></li>
<li>Ivan recently took a job at <a href="https://www.inkandswitch.com/">Ink &amp; Switch</a> on the "Ink" research track.</li>
<li><a href="https://daily.jstor.org/how-computer-science-became-a-boys-club/">Programmer Bums</a>, or, rather, <a href="https://www.jstor.org/stable/10.1086/682955?mag=how-computer-science-became-a-boys-club">Computer Bums</a></li>
<li><a href="https://www.youtube.com/watch?v=GceNsojnMf0">Limmy's Wa</a></li>
<li><a href="https://retool.com/">Retool</a></li>
<li><a href="https://en.wikipedia.org/wiki/MythBusters">MythBusters</a></li>
<li><a href="https://en.wikipedia.org/wiki/The_Flop_House">The Flop House</a>'s <a href="https://flophousepodcast.fandom.com/wiki/Final_Judgments">Final Judgements: Good-Bad, Bad-Bad, Kinda-Like</a></li>
<li><a href="https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type">CRDT</a></li>
<li><a href="https://en.wikipedia.org/wiki/Data_(Star_Trek)">Data</a></li>
<li><a href="https://andrewwalpole.com/blog/an-introduction-to-robust-first-computation/">Robust-First Computing</a> is an approach championed by the hero <a href="https://hachyderm.io/@livcomp">Dave Ackley</a>, and I have a well-informed hunch that you'll be hearing a lot more about it in future episodes.</li>
<li><a href="https://www.youtube.com/watch?v=jreRFxN6wuM">The T2 Tile Project</a> is another Ackley joint that, perhaps, works as a wild example of what Mary Shaw means when she talks about an "execution ecosystem".</li>
<li><a href="https://xxiivv.com/">Devine</a>'s talk at Strange Loop: <a href="https://www.youtube.com/watch?v=T3u7bGgVspM">An approach to computing and sustainability inspired from permaculture</a></li>
<li><a href="https://en.wikipedia.org/wiki/MUMPS">MUMPS</a> (the medical thing, not to be confused with <a href="https://en.wikipedia.org/wiki/Mumps">mumps</a> the medical thing) is used by <a href="https://en.wikipedia.org/wiki/Epic_Systems">Epic</a> (the software company, not to be confused with <a href="https://en.wikipedia.org/wiki/Epic_Games">Epic</a> the software company).</li>
<li>The <a href="https://www.glasscannonnetwork.com/">Glass Cannon</a> podcast network.</li>
<li>Lu's SPLASH talk <a href="https://www.youtube.com/watch?v=cBYudbaqHAk&amp;t=6704s">Cellpond: Spatial Programming without Escape</a></li>
<li>The <a href="https://en.wikipedia.org/wiki/Turing_tarpit">Turing tarpit</a></li>
<li><a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.125">Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire</a> by Erik Meijer, Maarten Fokkinga, Ross Paterson.</li>
<li><a href="https://en.wikipedia.org/wiki/Aphex_Twin">Richard D. James</a> is the same person as <a href="https://en.wikipedia.org/wiki/Richard_P._Gabriel">Richard P. (Peter) Gabriel</a>, right?</li>
<li>Similarly, see <a href="https://en.wikipedia.org/wiki/Neil_Armstrong">Neil Armstrong</a>'s work on <a href="https://en.wikipedia.org/wiki/Erlang_(unit)">Erlang</a> (which is popular in telephony, right?).</li>
<li><a href="https://en.wikipedia.org/wiki/The_Witness_(2016_video_game)">The Witness</a> is not going to appear in our show notes.</li>
<li><a href="https://jackrusher.com/">Jack Rusher</a>. <a href="https://berlin.social/@jack">Jack Rusher</a>? <a href="https://futureofcoding.org/episodes/041">Jack Rusher</a>!</li>
<li><a href="https://www.youtube.com/watch?v=9qVT0URkkGE">TrainJam</a></li>
<li><a href="https://www.destroyallsoftware.com/">Gary Bernhardt</a>'s talk <a href="https://www.destroyallsoftware.com/talks/ideology">Ideology</a></li>
</ul>
Nobody remarked on these silly links last time, so this time I'm drawing more attention to them:
<ul>
<li>Tode: <a href="https://mas.to/@todepond">Neopets</a> • <a href="https://www.patreon.com/todepond">MySpace</a></li>
<li>Berd: <a href="https://mas.to/@todepond">Angelfire</a> • <a href="https://www.patreon.com/todepond">Orkut</a></li>
<li>Bot: <a href="https://mas.to/@todepond">Geocities</a> • <a href="https://www.patreon.com/todepond">Friendster</a></li>
</ul>
<a href="https://futureofcoding.org/episodes/069">https://futureofcoding.org/episodes/069</a>

Myths & Mythconceptions by Mary Shaw

The subject of this episode's paper — Propositions as Types by Philip Wadler — is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. Everything — life, space, time, existence — all of it is a joke! A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once:
General recursive functions by Gödel in 1934, with functions of sets of natural numbers.
Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions.
Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape.

Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not without precedent. But then it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program.

The implications boggle the mind. How could this be so? Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation?

Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more.

And we are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadler's paper (and the much more approachable Strange Loop talk), and tying it in with the cultural context of modern functional programming, we hope you'll gain an appreciation for this remarkable, divine pun that sits beneath all of computation.

Links

=> patreon.com/futureofcoding — but only if you back the Visual Programming tier!! I'm warning you!
Wadler's Strange Loop talk Propositions as Types
Cocoon is good. It's not, like, Inside or Limbo good, but it's good. Actually, just play Inside. Do that ASAP.
Hollow Knight, also extremely good. Can't wait for Silksong. But seriously, if you're reading this and have haven't played Inside, just skip this episode of the podcast and go play Inside. It's like 3 hours long and it's, like, transformatively great.
Chris Martens has done some cool work (eg) bringing together linear logic and games.
Meh: Gödel, Escher, Bach by Douglas Hofstadter
Yeh: Infinity and the Mind by Rudy Rucker
Heh: To Mock a MockingBird by Raymond Smullyan.
The hierarchy of automata
Games: Agency as Art
The Incredible Proof Machine is what some would call a "visual programming language" because proofs are programs. But it's actually really cool and fun to play with. Approach it like a puzzle game, and give it 10 minutes or so to get its hooks into you.
"Stop Doing Logic" is part of the Stop Doing Math meme. Unrelated: Ivan's song Don't Do Math.
Bidirectional Type Checking, a talk by David Christiansen
List Out of Lambda, a blog post by Steve Losh

Nobody noticed that these links were silly last time, so this time I'm drawing more attention to it:
Ivan: Mastodon • Email
Jimmy: Mastodon • Twitter

This link is legit:
DM us in the FoC Slack

https://futureofcoding.org/episodes/068

The subject of this episode's paper — <a href="https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf">Propositions as Types</a> by <a href="https://en.wikipedia.org/wiki/Philip_Wadler">Philip Wadler</a> — is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. Everything — life, space, time, existence — all of it is a joke! A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once:
<ul>
<li>General recursive functions by Gödel in 1934, with functions of sets of natural numbers.</li>
<li>Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions.</li>
<li>Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape.</li>
</ul>
Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not <a href="https://en.wikipedia.org/wiki/Multiple_discovery">without precedent</a>. But then it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program.
The implications boggle the mind. How could this be so? Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation?
Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more.
And we are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadler's paper (and the much more approachable <a href="https://www.youtube.com/watch?v=IOiZatlZtGU">Strange Loop talk</a>), and tying it in with the cultural context of modern functional programming, we hope you'll gain an appreciation for this remarkable, divine pun that sits beneath all of computation.
Links
=&gt; <a href="https://www.patreon.com/futureofcoding">patreon.com/futureofcoding</a> — but only if you back the Visual Programming tier!! I'm warning you!
<ul>
<li>Wadler's Strange Loop talk <a href="https://www.youtube.com/watch?v=IOiZatlZtGU">Propositions as Types</a></li>
<li><a href="https://www.cocoongame.com/">Cocoon</a> is good. It's not, like, <a href="https://playdead.com/games/inside/">Inside</a> or <a href="https://playdead.com/games/limbo/">Limbo</a> good, but it's good. Actually, just play Inside. Do that ASAP.</li>
<li><a href="https://www.hollowknight.com/">Hollow Knight</a>, also extremely good. Can't wait for <a href="https://hollowknightsilksong.com/">Silksong</a>. But seriously, if you're reading this and have haven't played Inside, just skip this episode of the podcast and go play Inside. It's like 3 hours long and it's, like, transformatively great.</li>
<li><a href="https://www.convivial.tools/">Chris Martens</a> has done some cool work (eg) bringing together linear logic and games.</li>
<li>Meh: <a href="https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach">Gödel, Escher, Bach</a> by Douglas Hofstadter</li>
<li>Yeh: <a href="https://en.wikipedia.org/wiki/Infinity_and_the_Mind">Infinity and the Mind</a> by Rudy Rucker</li>
<li>Heh: <a href="https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird">To Mock a MockingBird</a> by Raymond Smullyan.</li>
<li>The <a href="https://en.wikipedia.org/wiki/Automata_theory">hierarchy of automata</a></li>
<li><a href="https://www.goodreads.com/book/show/48765399-games">Games: Agency as Art</a></li>
<li><a href="http://incredible.pm/">The Incredible Proof Machine</a> is what some would call a "visual programming language" because proofs are programs. But it's actually really cool and fun to play with. Approach it like a puzzle game, and give it 10 minutes or so to get its hooks into you.</li>
<li>"Stop Doing Logic" is part of the <a href="https://knowyourmeme.com/memes/stop-doing-math">Stop Doing Math</a> meme. Unrelated: Ivan's song <a href="https://ivanish.ca/dont-do-math/">Don't Do Math</a>.</li>
<li><a href="https://www.youtube.com/watch?v=utyBNDj7s2w">Bidirectional Type Checking</a>, a talk by <a href="https://davidchristiansen.dk/">David Christiansen</a></li>
<li><a href="https://stevelosh.com/blog/2013/03/list-out-of-lambda/">List Out of Lambda</a>, a blog post by <a href="https://stevelosh.com/">Steve Losh</a></li>
</ul>
Nobody noticed that these links were silly last time, so this time I'm drawing more attention to it:
<ul>
<li>Ivan: <a href="https://mas.to/@todepond">Mastodon</a> • <a href="https://www.patreon.com/todepond">Email</a></li>
<li>Jimmy: <a href="https://mas.to/@todepond">Mastodon</a> • <a href="https://www.patreon.com/todepond">Twitter</a></li>
</ul>
This link is legit:
<ul>
<li>DM us in the <a href="https://futureofcoding.org/community">FoC Slack</a></li>
</ul>
<a href="https://futureofcoding.org/episodes/068">https://futureofcoding.org/episodes/068</a>

Unison's Paul Chiusano on how Abstraction Will Save Distributed Computing

In 1 playlist(s)

Future of Coding

Social links

Recent clips