"If we can extend an extensible type and reimplement its interface (and re-prove its invariant) so that the new implementation/proof is observationally equal to the original as far as the original cases are concerned, then our extension may as well have been part of the type all along."
"This take on the expression problem can easily generalize it to cubes, to say the least!"
Solve ALL the expression problems!
---
"I don't particularly intend for my system to support induction or recursion, at least at the proof level. It's great to be able to manage infinite families of value given only finite tools, but I see that as more of a nice-to-have feature, less essential than the modularity and convenience I'm trying to establish."
"I'm interested in demonstrating that this system ties into the foundation of mathematics with multiple relative consistency results, and ironing out any paradoxes along the way. However, I'm even more motivated to expand my model into a full programming language. With any luck, that'll help on the way to those proofs."
