So I had been planning to give a talk at OS Bridge until, well, the night before Bridge started my body thought it would be a great time for my immunue system to collapse in on itself and leave me stuck in bed for four days straight. I was planning to give a talk that was more or less a condensation of the course I taught last term into ~40 minutes and pretty much just hitting only the highlights.
The basic take aways I was going to try and get across is that
- understanding the limitations of what a computer can do is good for your soul
- computation is a really really limited subset of mathematics
- constructive logic gives meaning to our types (while possibly giving up Turing completeness)
The reason why I say “possibly” giving up Turing completeness is that in a sense if you have coinduction you really do have all the computable functions at your disposal and because there are languages such as Idris that allow you to choose to allow general recursion in limited settings while still insisting upon totality when you want types-as-theorems.
I’m including the link to the repo where I put my slides. I don’t entirely know how useful they’ll be since there’s a lot I was going to say that wasn’t necessarily explicit as bullet points but, hey, why not link to it! The slides are mostly complete but I might end up adding some things to them to be a bit more explicit about some topics near the end where it’s a little rushed.