Other people have taken that approach, for example the HALO project in Haskell. But the imprecision of the defunctionalizaton often makes it hard to prove the p

Other people have taken that approach, for example the HALO project in Haskell. But the imprecision of the defunctionalizaton often makes it hard to prove the properties you want, especially without static types.