Honestly, from what I see, the amount you do is relatively minuscule compared with what Opera was doing ten years ago, while Opera had far more marketshare which is normally the best way to avoid web compat issues in the first place.
It's a rule of thumb in most software I found studying high-assurance. Inevitably, some academic or commercial team wants to robustly implement some standard (esp a protocol). They notice it's specified in a combo of English and implementation code. They start doing formal specifications of English spec. Every time, IIRC, they find various inconsistencies and such that already did or could lead to real-world problems. Showed me the value of formal specs but also important lesson: using informal specs will almost always require reverse engineering and extensive testing due to, at very least, English ambiguity or implementation deviations.
Implementing SIP a couple of times, part of it is the other implementations just flat-out misread. Even when there's a formal syntax specified, they simply ignore it. For instance, SIP specifies a "lr" (loose route) parameter. The syntax is just that: lr. But many implementations get it wrong and require a value, like lr=1, or lr=true.
Even things as simple as line endings are implemented wrong (in HTTP too), and that can cause security consequences as proxies end up reading headers differently than the user agents. I've seen this live on the public Internet.
SIP and the IETF to some extent encourages this with Postel's Law, telling implementors they should guess what the intention of the message is. We need less of VB's On Error Resume Next and more panic-abort type functionality. Look at this insane document: https://tools.ietf.org/html/rfc4475 "SIP Torture Tests". The authors gleefully come up with ridiculous yet legal permutations of messages that are allowed under their arcane rules. The fact this exists should send the opposite message: simplify your damn protocol. And this is only at the parsing level!
I know people say that HTML could never have had strictness because it'd have been too hard, but I don't buy that. One common issue was getting nesting wrong, like <b><i></b></i> or leaving unclosed tags. By removing the (silly, honestly) name out of the ending tag and just using </>, a whole class of errors is removed. Add in a browser that just fails to render and explains exactly why, and people would quickly not publish pages that are broken.
> SIP and the IETF to some extent encourages this with Postel's Law, telling implementors they should guess what the intention of the message is. We need less of VB's On Error Resume Next and more panic-abort type functionality.
I don't think it's as clear-cut as that. I think the main thing is error handling must be defined: it doesn't matter whether it's panic-abort or whether it's defined how to deal with any stream of bytes. Don't let implementers choose what they should do.
RFC 7230, for example, has error handling sometimes as SHOULD return 400 Bad Request and sometimes as MUST return 400 Bad Request. But that only applies to servers and proxies parsing requests, which are really the relatively well-implemented part of HTTP. (The vast majority come from browsers, which are always syntactically valid; responses can come from arbitrary CGI scripts and you get all kinds of syntactic nonsense there.) Sadly, there's comparatively few normative requirements when it comes to parsing responses, even ones which are needed for backwards compatibility (at what point do you conclude you're just talking to an HTTP/0.9 server?).
So most of the spec bugs I've come across don't have to do with English vagaries; they have to do with the reverse-engineering not being perfect. Converting the nebulous concept of expected behavior into procedural text is hard, and there are bugs.
So yeah, "implementation deviations" is usually the issue, but not really English ambiguity, at least with web specs. I put my pedant hat on when looking at proposed changes to web specs, and I believe the rest of the community does too :)
There have certainly been spec bugs that could be found from a formal specification, some of which are security related (most of the TLS bugs found by miTLS have been protocol bugs simply found as a result of encoding much of the semantics formally).
That said, while I certainly have a fondness for formal specifications, I also always end up feeling like they have a lot of downsides. They're often very verbose and hard to skim, and they're also another language that anyone implementing the specification has to learn prior to implementing it (or they can just wing it, but then your formal specification is worth nothing!).
The wisdom from old days was to use relatively, simple, formal languages that were easy to train people on and use. B, Z, and TLA had good results plus lasted over time. The other thing was to do English spec, formal spec, and code side-by-side with each team looking for inconsistencies. The developers usually picked up the basics of the technique rather quickly but at least one specialist was always necessary to make first use go smoothly.
So, that's still my recommendation. A subset of those, especially focusing on states and contracts, done in same fashion against English specs and clear code should take lower work than going all Isabelle, NuPRL, or PVS on a problem. Second application is also always easier. Reuse where possible helps as with code.
So, some difficulties and training but probably easier than some frameworks, etc IT people learn today.
(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.
Hmm. That's unusual situation. I've seen descriptions that sound similar in B data validation. For now, I'll just make a note of this comment to bring up when I next bump into formal methodists that might have answers.
