3 ms·
I 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 ver
by cantankerous 13y ago
I 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.