Although I was saving it for later, @hwayne posting this made me move it forward since she should be on the list. Both of us previously referenced Guttman’s work that shows about every way formal methods had failed at the time to give a reality check to overzealous post. His is undeniably the reference work on that. However, this woman had issued similar warnings over a decade earlier after trying to mechanically check the proof for the first, “verified” processor (VIPER) which already drew criticism from Computational Logic Inc folks that did the real first, verified stack (FM9001) later on.
At that time, Avra was tired of the overselling enough to use Section 6 to demolish any notion that people were verifying hardware then or maybe even later (now). She wanted the verification claims to be narrow with proper caveats like the verification itself was. Also, reinforced the notion of balancing multiple methods for assurance including non-formal.
Although I was saving it for later, @hwayne posting this made me move it forward since she should be on the list. Both of us previously referenced Guttman’s work that shows about every way formal methods had failed at the time to give a reality check to overzealous post. His is undeniably the reference work on that. However, this woman had issued similar warnings over a decade earlier after trying to mechanically check the proof for the first, “verified” processor (VIPER) which already drew criticism from Computational Logic Inc folks that did the real first, verified stack (FM9001) later on.
At that time, Avra was tired of the overselling enough to use Section 6 to demolish any notion that people were verifying hardware then or maybe even later (now). She wanted the verification claims to be narrow with proper caveats like the verification itself was. Also, reinforced the notion of balancing multiple methods for assurance including non-formal.