> Yeah, I was somewhat involved in the research behind that paper. I think > it's trying too hard to fit imperative style into a proofy language; it's > difficult to be direct with that approach and there are certain kinds of > constructions that are impossible with it (like getting the value you store > in a pointer-keyed hash table back out later). You still need a good > compiler to make the code efficient - this was a big problem in lean 3 and > lean 4 is solving it at great development expense. Here I think we do > better to just let the established programming languages do what they were > designed to do. >
Another recent research paper on the subject: "We introduce Perceus, an algorithm for precise reference counting with reuse and specialization. Starting from a functional core language with explicit control-flow, Perceus emits precise reference counting instructions such that programs are _garbage free_, where only live references are retained. This enables further optimizations, like reuse analysis that allows for guaranteed in-place updates at runtime. This in turn enables a novel programming paradigm that we call _functional but in-place_ (FBIP). Much like tail-call optimization enables writing loops with regular function calls, reuse analysis enables writing in-place mutating algorithms in a purely functional way. We give a novel formalization of reference counting in a linear resource calculus, and prove that Perceus is sound and garbage free. We show evidence that Perceus, as implemented in Koka, has good performance and is competitive with other state-of-the-art memory collectors." https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/ -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5582bc04-1e13-4ee8-ae33-3adb87f1a805n%40googlegroups.com.
