Subscribe: Mathematics and Computation
http://math.andrej.com/feed
Preview: Mathematics and Computation

Mathematics and Computation



Mathematics for computers



Last Build Date: Wed, 07 Sep 2016 08:42:19 +0000

 



The new and improved Programming languages zoo

Wed, 07 Sep 2016 08:39:16 +0000

It is my pleasure to announce the new and improved Programming languages Zoo, a potpourri of miniature but fully functioning programming language implementations. The new zoo has a decent web site, it is now hosted on GitHub, and the source code was cleaned up. Many thanks to Matija Pretnar for all the work. The purpose of … Continue reading The new and improved Programming languages zoo



Formal proofs are not just deduction steps

Tue, 30 Aug 2016 15:08:36 +0000

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. In traditional mathematical logic (by which I mean first-order logic, as established by Hilbert, Ackermann, Skolem, Gödel and others) the concepts of logical formula and formal proof are the central notions. This … Continue reading Formal proofs are not just deduction steps



What is a formal proof?

Tue, 09 Aug 2016 12:28:11 +0000

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 … Continue reading What is a formal proof?



Hask is not a category

Sat, 06 Aug 2016 20:36:40 +0000

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. Let us look at the matter a bit closer. The Haskell … Continue reading Hask is not a category



The Andromeda proof assistant (Leeds workshop slides)

Thu, 28 Jul 2016 13:28:41 +0000

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 … Continue reading The Andromeda proof assistant (Leeds workshop slides)