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

Mathematics and Computation



Mathematics for computers



Last Build Date: Mon, 10 Oct 2016 15:43:20 +0000

 



Five stages of accepting constructive mathematics

Mon, 10 Oct 2016 15:27:59 +0000

In 2013 I gave a talk about constructive mathematics “Five stages of accepting constructive mathematics” (video) at the Institute for Advanced Study. I turned the talk into a paper, polished it up a bit, added things here and there, and finally it has now been published in the Bulletin of the American Mathematical Society. It is … Continue reading Five stages of accepting constructive mathematics



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