The way this article talks about using "recursive real arithmetic" (RRA) reminds me of an excellent discussion with Conal Elliot on the Type Theory For All podcast. He talked about moving from representing things discretely to representing things continually (and therefore more accurately). For instance, before, people represented fonts as blocks of pixels, (discrete.) They were rough approximations of what the font really was. But then they started to be recognized as lines/vectors (continual), no matter the size, they represented exactly what a font was.
Conal gave a beautiful case for how comp sci should be about pursuing truth like that, and not just learning the latest commercial tool. I see the same dogged pursuit of true, accurate representation in this beatiful story.
Thanks, that's a lovely analogy and I'm excited to listen to that podcast.
I think the general idea of converting things from discrete and implementation-motivated representations to higher-level abstract descriptions (bitmaps to vectors, in your example) is great. It's actually something I'm very interested in, since the higher-level representations are usually much easier to do interesting transformations to. (Another example is going from meshes to SDFs for 3D models.)
Conal gave a beautiful case for how comp sci should be about pursuing truth like that, and not just learning the latest commercial tool. I see the same dogged pursuit of true, accurate representation in this beatiful story.
- https://www.typetheoryforall.com/episodes/the-lost-elegance-...
- https://www.typetheoryforall.com/episodes/denotational-desig...