I am discovering that mathematicians cannot tell the difference between “proof by contradiction” and “proof of negation”. This is so for good reasons, but conflation of different kinds of proofs is bad mental hygiene which leads to bad teaching practice and confusion. For reference, here is a short explanation of the difference between proof of negation and proof by contradiction. Continue reading Proof of negation and proof by contradiction

# Category Archives: Tutorial

# Tutorial on exact real numbers in Coq

Already a while ago videolectures.net published this **tutorial on Computer Verified Exact Analysis** by Bas Spitters and Russell O’Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also gave a quick tutorial on Coq.

# On programming language design

In a recent post I claimed that Python’s lambda construct is broken. This attracted some angry responses by people who thought I was confused about how Python works. Luckily there were also many useful responses from which I learnt. This post is a response to comment 27, which asks me to say more about my calling certain design decisions in Python crazy.

# Intuitionistic mathematics for physics

At MSFP 2008 in Iceland I chatted with Dan Piponi about physics and intuitionistic mathematics, and he encouraged me to write down some of the ideas. I have little, if anything, original to say, so this seems like an excellent opportunity for a blog post. So let me explain why I think *intuitionistic mathematics is good for physics*.

Continue reading Intuitionistic mathematics for physics

# Representations of uncomputable and uncountable sets

Occasionally I hear claims that uncountable and uncomputable sets cannot be represented on computers. More generally, there are all sorts of misguided opinions about representations of data on computers, especially infinite data of mathematical nature. Here is a quick tutorial on the matter whose main point is:

It is

meaninglessto discuss representations of a set by a datatype without also considering operations that we want to perform on the set.

Continue reading Representations of uncomputable and uncountable sets