(As a disclaimer, for some context, I have only relatively passing experience with Z, and the majority of formal modelling of specs I've done is using CSP.) Fr

(As a disclaimer, for some context, I have only relatively passing experience with Z, and the majority of formal modelling of specs I've done is using CSP.) From when I've considered trying to formalise parts of the platform before, some of the things that often get hit very quickly are the fact that most of the web platform is defined in terms of sequences of Unicode code points, and ultimately any formalisation is going to have to deal with that (be it some complex parser—like HTML—or some simple validation of it matching a regular grammar). It has always seemed to me that to get much advantage you need to be able to programmatically assert statements about it (including, most obviously, pre-conditions are satisfied at all call-sites), but once you've gone from 2^256 to 2^1114112 characters you end up with such massive state explosion that even many symbolic tools start to struggle quickly. Now, maybe I've tried using the wrong tools, or maybe I'm structuring things wrong, but it'd be nice to have some way to do this.