I suspect that constructing your models with these logical rules and running them and their interactions through a proof checking compiler like Haskell's could help with concurrency, security, large code bases, refactoring and more. And yet what we get are solutions to problems that we don't really have.