Dedekind-cut formalizations of the reals appear now and then in theorem-proving settings (e.g. Coq provides one), but this is the first implementation I've foun

Dedekind-cut formalizations of the reals appear now and then in theorem-proving settings (e.g. Coq provides one), but this is the first implementation I've found in a normal programming language. I was looking for one for pedagogical purposes, hoping for a real-number analog to the ubiquitous Peano-arithmetic examples that you find in SICP and other texts. This is probably a bit too complex for those purposes, especially since it proceeds by first recasting the Dedekind construction in a new formalism rather than the classic set-theoretic definition. But I found it interesting anyway.