Oh, that's interesting. I think the main thing that turned me away from more typical persistent data structures was my assumption that the proof size would be unacceptably large (also that branch rewrites during insertion would cause too much growth). A solution to that would be amazing. I'll try to grok this later tonight.
Happy to discuss and dive in. We’ve been thinking about this problem for quite some time.
JP was supposed to put us in touch last year, as we had questions on Urkel, but it never happened.
Happy to connect here.
