Three Dollar Quill

I've got a rough outline of the transformations I want to do to Impliciula code, with the general idea that LLVM IR is like the simply-typed lambda calculus, except that there are a bunch of things that can go wrong, which the higher levels need to deal with. (And there are modules, so, like, something involving existential types happened, I guess. And probably other things.) However.

Once I put the thought in properly, I realized that basic closure-based handling of resource lifecycles, while sufficient for many purposes, simply won't cut it for all use cases. So, if I want verifiably safe pointer manipulation that's also flexible, I need to also be reading up on substructural type systems, specifically affine types. My hope is that I can somehow connect this to refinement types so that it's possible to construct custom theories of pointer lifecycles. If I can't make that work, then I kind of need to reevaluate the whole direction I'm taking this project.

I have no idea whether I should expect that to work, but if it doesn't... ugh. Anyway, I'll have a better idea whether it will or not once I do some more reading, so I'm going to wrap this up now.

Good night.