Tady jsou příklady témat, co jsem měl na mysli:
https://leanprover.github.io/talks/IFL2019.pdf
https://arxiv.org/pdf/1908.05647.pdf
https://dl.acm.org/doi/pdf/10.1145/3547640
Ta lokální imperativita přeskládá kód s mutabilními proměnnými do “do” bloků (pomocí bind) v čistě funkcionálním jazyce. A ten FBIP zaručí čistě funkcionální datové struktury s výkonem mutabilních (když je refcount 1). Pokud jsou všechny funkce totální a všechny typy induktivní, znamená to, že program vždy skončí a zaručeně nemá memory leaky. Což jinak zaručí jen tracing GC, akorát že nedeterministicky. Jsem k dispozici k případným dotazům :)