4 ms·

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

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.

AnimalMuppet 9y ago
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).
- catnaroek 9y ago
  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.
dan_mctree 9y ago
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.
- ScottBurson 9y ago
  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.

AnimalMuppet 9y ago

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).

catnaroek 9y ago
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.

dan_mctree 9y ago

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.

ScottBurson 9y ago
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.