Addition, as I missed the edit window.

I wish they would elaborate on what Really Really Hard(tm) means. From a high-level I believe everything they are concerned with has been researched as part of the work on contract by Robby Findler and collaborators. E.g. https://users.cs.northwestern.edu/~robby/pubs/papers/popl201...