Hacker News Reader

Comment by AnimalMuppet | Hacker News Reader

How long have you worked as a professional programmer? Because you sound like a just-out-of-school idealist with an idea of the "right way to do it". That ideal tends to get blunted after a decade or two of experience in the real world.

In particular: Set theory? I don't want to program using set theory for the same reason that I don't want to program using octal - it's the wrong level of abstraction for what we're actually doing, no matter whether it's formally equivalent or not.

Tools for checking the correctness of desired properties? I can agree with you there; better tools for doing so would be useful. So far, the problem tends to be that the tools are less generally useful than the tools' authors and proponents think they are.

View on HN

I don't know what kind of code you've been writing, but I've been working in compilers and static analysis for decades, and set theory is exactly the right tool for the job. I don't imagine it's the only thing you would ever need for any kind of programming, but I bet there aren't many kinds of programming to which it is entirely irrelevant.

The quality of the vast majority of my code is evaluated in 'soft' ways. Anywhere from "does this webpages layout work well on all browsers" to "does this AI feel like a challenging opponent" to "did you deliver software results fast enough" to "is the code neat enough and well documented". The part that can be meaningfully tested through any kind of formal system or automation is minuscule and it's very rarely where the problems lie.

What you're talking about is what I call the "specification-implementation gap". In some domains, that gap is vanishingly small; webpage layout is a good example. Sometimes the specification is as simple as "when the user clicks this button, display this message". There's nothing to be gained by formally verifying that particular property of the specification.

But sometimes the gap is wider. An only slightly more complex example would be "the shopping cart contains all items added to it in the current session and not subsequently removed". Sounds trivial, right? Well, as it happens, just a couple of days ago I bought two items from a site whose cart was broken -- it would show only the most recently added item. (I had to make two transactions. Fortunately no shipping fees were involved.) Okay, that's a rare sort of bug, but it just shows how even very simple invariants can get broken on occasion.

Sometimes the gap is even wider. "This app must have no XSS vulnerabilities." There's no one place in the program where you can see that that property is correctly implemented.

You see where I'm going with this: the wider the specification-implementation gap, the more useful formal methods can be.

For static analysis, OK. For a compiler, OK. But I want the static analyzer and the compiler to do that so that I don't have to - I don't want to have to think in set theory to program.

And in saying that, I see that I was probably unfair to haskellandchill's point. The claim wasn't that I needed set theory; the claim was that the tools needed it (at least, so it appears to me on re-reading).

Not every program property of interest can be (conveniently) verified using automated tools - especially if your verification tool is a type checker! Sometimes you need to roll up your sleeves and prove things yourself. (Which, by the way, isn't always a bad thing.)

That being said, hopefully you won't have to use set theory, where any structure that actually matters to you has to be encoded in terms of sets containing sets containing sets, until you reach turtles.

8 years of web dev under my belt, but yes I do have some academic pedigree and have been investing my time heavily in the history and techniques of formal methods. I'm hoping to contribute to bridging the gap. Don't get too hung up on set theory, I was just referencing the article.

It is my impression (as an outsider) that web programming might be the hardest environment for formal methods. Yes, I could see formal methods proving that only valid HTML was ever emitted. But how do you prove that your layout aligns on Firefox 55.0.3?

So it seems to me that, if you can make progress on formal methods in your environment, you're not picking low-hanging fruit...

> I could see formal methods proving that only valid HTML was ever emitted.

I think we could also prove the absence of XSS vulnerabilities. That would be very valuable.

> But how do you prove that your layout aligns on Firefox 55.0.3?

This is harder, admittely. Mozilla is probably not going to provide the formal model that haskellandchill imagines, unless that model can be automatically extracted from the actual code, which may be possible someday.

If FireFox provided a formal model of how it lays things out I can prove I use it correctly in my code. It's about trust and providing models for other programmers to use in their proofs along with our code. Or code and proofs can be even more intertwined, since they are very related.

Interesting point.

It's hard to prove theorems without the [correct] axioms.

I suppose what our field needs to do is some "triage" categorizing aspects of systems that MUST be "defined and proven" vs those that can be "intuited" - e.g. - back-end database updates need to be correct, but it's acceptable to have the user reload a web page if something crashes occasionally???

But The Man wants lots of 'wares made by cheap full stack developers, er, dev-ops :-(

Reply on news.ycombinator.com