5 ms·
How do you formally prove that a GUI is "usable"? How do you formally prove that a game is "fun"? How do you even know what you should be formally proving? For
by brandonbloom 13y ago
How do you formally prove that a GUI is "usable"? How do you formally prove that a game is "fun"? How do you even know what you should be formally proving?
Formal proofs (and type systems too) can only prove that your programs and formal specifications are internally consistent. The overwhelming largest set of failures in commercial software development are in requirements solicitation!
"Mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true." - Bertrand Russell
There is a very high initial and maintenance cost to proofs and it would be a mistake to insist that people pay that cost when better cost/benefit trade offs exist for most needs.
- cantankerous 13y agoI think the OP is asking about when what you mentioned in your second paragraph is going to become the industry standard. Nobody's going to be using formal verification to prove that something is usable or fun. Automated proof checking and derivations systems have been under development and research for a long time now. It's almost just an engineering problem to introduce them in a way that commercial companies can use them. The aerospace industry (ex Boeing) has been doing this for a long time, and they make it work quite well for them.
- brandonbloom 13y ago> Boeing) has been doing this for a long time Sure, and Microsoft has been using formal methods for eliminating all manner of security holes since at least the XP SP2 days. I didn't say that formal methods were always a bad trade off. I said that they are very expensive and implied that they are a bad default tradeoff for general purpose tools to make.
- Altenuvian 13y agocould you point to documents explaining proof checking in aerospace industry? I am especially interested in the history leading to software verification in avionics, the involvement of insurance companies and government regulation. thx
- cantankerous 13y agoI actually cannot off hand. I speak from meeting folks in the industry who actually do the proof checking for aeronautical software. Unfortunately some dude's word on the Internet probably isn't very appealing. I'm sure Google would pull something up, though.
- oakwhiz 13y agoI think the idea here is to guard against crashes and security violations, not whether software is able to accomplish some goal or not.