5 ms·
And pray tell how do you verify that the parser is actually correct? How strict can you get? Lax parsers are the bane of every web browser's existence. Ultima
by AstralStorm 6y ago
And pray tell how do you verify that the parser is actually correct? How strict can you get?
Lax parsers are the bane of every web browser's existence.
Ultimately parsing does not get you to correctness, ensuring properties does, and a type system is the lamest way to do it. There are actual logic solvers/theorem provers that can handle properties and are as powerful as programming languages while also ensuring correctness and most importantly completeness.
Some of them were even available as extensions for Java, though constraint programming is not currently in the mainstream. (Besides a small variant called borrow checking, used in Rust for instance.)
- wvenable 6y agoLax parsers made the modern web possible. New web pages with image tags, forms, and scripts were possible without breaking that page's parsing in older browsers.
- jcelerier 6y ago> Lax parsers made the modern web possible. that's the whole problem indeed
- deleted 6y ago[deleted]
- jacobush 6y agohttps://mcshowblog.files.wordpress.com/2019/08/dumpsterfire.jpg https://mcshowblog.files.wordpress.com/2019/08/dumpsterfire.... Yeah bad example if you wanted to convince me it’s any good :-D
- anoncake 6y agoThat's like saying sloppy programming makes software development possible. At best, it speeds things up (a temporary benefit) at the cost of quality (causing potentially permanent damage).
- harperlee 6y agoThat’s not like what was said above. They said that a strict parser would choke on unrecognized tags, thus making experimentation non-viable. Sloppy programming is not about enabling new syntax at all. That simile is not useful.
- KirinDave 6y agoI think that at this point, folks have realized this is not in fact true. If anything, lax parsers made the evolution of the web more difficult and more subject to corporate cooption.
- wvenable 6y agoWhat's the argument for that? If HTML was strictly parsed the first page with an image tag would have been broken in all other browsers.
- morelisp 6y agoIgnoring for one second the specifics of <img> in relation to SGML's `O` option (which was rectified in XML), this doesn't really need to have been the case. HTML could easily have said "if you encounter an unknown tag, render its contents as PCDATA" and sites would have degraded at least as gracefully as they do today. (If less gracefully than they did in 2000.) (Heck, it could've been a generic SGML feature! "Unknown elements' contents are CDATA, unless they have this attribute in which case they're PCDATA, or this attribute in which case they're ignored" as a rule the DTD...)
- wvenable 6y ago> HTML could easily have said... But it didn't! The problem with being strict here is that every possible usage has to be pre-imagined and perfectly implemented. You're suggesting the original developers should have just made affordances for everything that will be added in the next 30 years. That's easy to say now. The first web browser was essentially just a hugely successful prototype. And can you imagine having to type all your tags in upper-case? Yuck. :)
- erik_seaberg 6y agoWe never needed to parse tag soup. We only needed to say which DTD defines the new elements a document uses, and what a browser should do with valid but unknown elements. The latter could use #FIXED or default attribute values in the DTD, because some new elements have human-readable content and others don’t.
- goto11 6y agoThis is not due to lax parsing though. It is due to the convention of how to process undefined tags and attribute: User agents must treat elements and attributes that they do not understand as semantically neutral; leaving them in the DOM (for DOM processors), and styling them according to CSS (for CSS processors), but not inferring any meaning from them. https://html.spec.whatwg.org/multipage/infrastructure.html#extensibility-2 https://html.spec.whatwg.org/multipage/infrastructure.html#e... This is unrelated to parsing - for example a XHTML parser will be strict and draconian in its parsing, but still process undefined tags and attributes as above.
- klodolph 6y ago> And pray tell how do you verify that the parser is actually correct? How strict can you get? The idea presented in the article is that the data type of the parser output ensures that your invariants are satisfied. It’s not a panacea for solving every possible problem with input validation, it’s more of an alternative technique that gives you much better assurances that some of the invariants you think should be satisfied, are satisfied.
- cptskippy 6y agoThe point of input validation is to fail early, not to ensure the function executes. Returning an empty list when the input is an invalid list sounds like a really bad idea. What if the function is deleteWhereNotIn( list param )? That empty list just deleted everything.
- lambda_obrien 6y agoThe original article was in a Haskell context, where you'd use a Maybe or Either to prevent that sort of mistake.
- a1369209993 6y ago> The point of input validation is to fail early, not to ensure the function executes. > What if the function is deleteWhereNotIn( list param )? error: could not assign `param` = `mungeList foo` note: failed to match `List a` <= `Either SomeError (List b)` note: failed to match `List` <= `Either SomeError`
- KirinDave 6y agoYou should read Alexis King's articles on how this is achieved. One of the most imporant aspects of modern parser combinator libraries is that a very small composable core can be exhaustively tested (importantly: with both hand written and random cases) to provide a reliable kernel for parser combinators. Given that those cited parsers were built from the ground up to mesh with an effective and expressive type system like Haskell's, this problem was significantly reduced. The downside, of course, is that it became quite opinionated. There is no magic want to wave, but certainly it's easier to work on a common minimal core of components than work on custom ad hoc validators. Lax parsers are not an inevitable outcome; they're a decision propagated by decades of bad opinions being taken as gospel.
- one-punch 6y agoAn expressive language should let programmers reason about code, including parsers, for their correctness. You know it is correct when you see it, and you get more confidence in not making silly mistakes with unit tests. This is a different approach to formal verification using logic solvers or theorem provers. For an example of parsing with Haskell, see this recent discussion: https://news.ycombinator.com/item?id=25212372 https://news.ycombinator.com/item?id=25212372 This approach, as hinted in Parse, Don’t Type-Check, is to raise the level of abstraction. The jargons are to create a domain-specific language (DSL) to model the problem, as in language-oriented programming. With this approach, you understand what the code is trying to do and can change it easily because it reads like pseudo-code. (Pseudo-code is usually a synonym for code at the right level of abstraction.)