This is a story close to my heart. Apparently, the Android calculator app uses recursive real arithmetic for some of its operations (though not everywhere, to limit the impact of undecidability). Bizarrely, the illustration under “constructive real numbers” does not show constructive real numbers, but otherwise — a nice and surprising writeup.