A Brainfuck interpreter written in Agda
The heart of the interpreter is a run function that, given a
Brainfuck program and the stream of characters entered via stdin,
produces a (possibly infinite) execution trace.
This program demonstrates how a total language, such as Agda, can
still be Turing complete – the run function assigns semantics to
any Brainfuck program, even those that do not terminate. The key
insight (which is not particularly novel) is that (productive)
coinductive programs are total and sufficient to simulate Turing
machines. For a more precise definition of 'total', I'd refer to David
Turner's work.