[xiphias2]

Is it still a big burden if the theorem prover can automate checking that a function can be evaluated without ref counting / garbage collector? I understand that it's a very hard problem though.