This isn't my field, but if I'm understanding correctly this is so cool. I love the idea of being able to unlock optimisations by formally specifying behaviour.
On a side note I chuckled at the following -
> Web browsers, for example, struggle to render modern web pages