They chose a method that's easier to prove. Imperative implementations are much harder to verify than functional. It's not that we can't do it, it's just really hard to do in practice so even people who verified the first compression bailed on the idea.