Hacker News Reader

Lean 4 uses FBIP, but it looks like this paper is about something called FIP, which is related but about guaranteeing there are no allocations or deallocations. FBIP as I understand it is more about being able write functional code in a natural away while avoiding allocations or deallocations.

(I agree about Lean 4 as becoming a great general purpose language though!)

View on HN

I'm sure the details are different, but the general idea, to me, seems the same as the one descibed by Leo and Sebastian in https://arxiv.org/abs/1908.05647. Both Koka and Lean 4 use reference counting to know if it's safe to reuse a structure.

This paper (Daan is a collegue of Leo at MS Research) gives a different formalization and proofs. The file is still named "fbip.pdf" though :)

Reply on news.ycombinator.com