I have participated in a couple of lengthy discussions about formal proofs. I realized that an old misconception is creeping in. Let me expose it.
What is a formal proof?
Mike Shulman just wrote a very nice blog post on what is a formal proof. I much agree with what he says, but I would like to offer my own perspective. I started writing it as a comment to Mike’s post and then realized that it is too long, and that I would like to have it recorded independently as well. Please read Mike’s blog post first.
Hask is not a category
This post is going to draw an angry Haskell mob, but I just have to say it out loud: I have never seen a definition of the so-called category Hask and I do not actually believe there is one until someone does some serious work.
The Andromeda proof assistant (Leeds workshop slides)
I am about to give an invited talk at the Workshop on Categorical Logic and Univalent Foundations 2016 in Leeds, UK. It’s a charming workshop that I am enjoing a great deal. Here are the slides of my talk, with speaker notes, as well as the Andromeda examples that I am planning to cover.
- Slides: AndromedaProofAssistant.pdf
- Andromeda files: nat.m31, universe.m31
The real numbers in homotopy type theory (CCA 2016 slides)
I am about to give an invited talk at the Computability and Complexity in Analysis 2016 conference (yes, I am in the south of Portugal, surrounded by loud English tourists, but we are working here, in a basement no less). Here are the slides, with extensive speaker notes, comment and questions are welcome.
Slides: hott-reals-cca2016.pdf