What Is Computation Anyway?

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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s