A nice think about this work is that adopting this strict model in real life codebases is going to bring to light cases where it isn't enough, and hopefully more scrutiny can be directed towards those cases.