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.

# Category Archives: Tutorial

# 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

# Seemingly impossible functional programs

Andrej has invited me to write about certain surprising functional

programs.

The first program, due to Ulrich Berger (1990), performs exhaustive

search over the “Cantor space” of infinite sequences of binary

digits. I have included references at the end. A weak form of

exhaustive search amounts to checking whether or not a total predicate

holds for all elements of the Cantor space. Thus, this amounts to

universal quantification over the Cantor space. Can this possibly be

done algorithmically, in finite time?

Continue reading Seemingly impossible functional programs