W3C home > Mailing lists > Public > public-html@w3.org > April 2007

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

From: Bruce Boughton <bruce@bruceboughton.me.uk>
Date: Sun, 15 Apr 2007 10:51:32 +0100
Message-ID: <4621F5A4.5000407@bruceboughton.me.uk>
To: Henri Sivonen <hsivonen@iki.fi>
CC: Henrik Dvergsdal <henrik.dvergsdal@hibo.no>, public-html@w3.org

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)

Received on Sunday, 15 April 2007 09:52:12 UTC

This archive was generated by hypermail 2.3.1 : Thursday, 29 October 2015 10:15:18 UTC