3 ms·

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 metho

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.

AnimalMuppet 9y ago
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...
- haskellandchill 9y ago
  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.
  - Roboprog 9y ago
    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 :-(
- ScottBurson 9y ago
  > 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.

AnimalMuppet 9y ago

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

haskellandchill 9y ago
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.
- Roboprog 9y ago
  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 :-(
ScottBurson 9y ago
> 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.