4 ms·
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 programm
by 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 agoInteresting 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 :-(