Re: Formal definition of HTML5 (was Re: Version information)

Henri Sivonen wrote:
> Furthermore, chances are that the conceptual model (appropriate for 
> the spec) and the sane data structures for a given application are 
> different. So different that if you had a formal language for 
> expressing constraints on the conceptual model, you couldn't trust an 
> inference engine to compile the constraints into a program that is as 
> space and time-efficient as a human-written program. For example, the 
> conceptual model for tables involves a grid of slots. Yet, it would be 
> an extremely bad idea for a table integrity checker to allocate 
> (colspan * rowspan * pointerSize) amount of memory when encountering 
> <td colspan='...' rowspan='...'>. (Why? Denial of service attacks 
> based on causing huge memory allocation requests.) I reasoned that the 
> HTML table slot allocation policy has certain properties and 
> consequences, which helped me come up with efficient data structures 
> and algorithms but I never drafted any formal proof that these 
> properties and consequences hold. In general, you don't prove your 
> programs correct using formal methods unless you are Knuth or unless 
> you are developing a control system for a rocket.
>

Presumably a browser UA would have to allocate that memory to build the DOM?

(I understand your general point that a conformance checker would have 
to be written in a Turing-complete language)

Bruce