Canonical software development examples emphasizing “proving safety/usefulness before running” over the “tool” software development approach are cryptographic libraries and NASA space shuttle navigation.
At the time of writing this comment, there was recent furor over software called CryptoCat that didn’t provide enough warnings that it was not properly vetted by cryptographers and thus should have been assumed to be inherently insecure. Conventional wisdom and repeated warnings from the security community state that cryptography is extremely difficult to do properly and attempting to create your own may result in catastrophic results. A similar thought and development process goes into space shuttle code.
It seems that the FAI approach to “proving safety/usefulness” is more similar to the way cryptographic algorithms are developed than the (seemingly) much faster “tool” approach, which is more akin to web development where the stakes aren’t quite as high.
EDIT: I believe the “prove” approach still allows one to run snippets of code in isolation, but tends to shy away from running everything end-to-end until significant effort has gone into individual component testing.
The analogy with cryptography is an interesting one, because...
In cryptography, even after you’ve proven that a given encryption scheme is secure, and that proof has been centuply (100 times) checked by different researchers at different institutions, it might still end up being insecure, for many reasons.
Examples of reasons include:
The proof assumed mathematical integers/reals, of which computer integers/floating point numbers are just an approximation.
The proof assumed that the hardware the algorithm would be running on was reliable (e.g. a reliable source of randomness).
The proof assumed operations were mathematical abstractions and thus exist out of time, and thus neglected side channel attacks which measures how long a physical real world CPU took to execute a the algorithm in order to make inferences as to what the algorithm did (and thus recover the private keys).
The proof assumed the machine executing the algorithm was idealized in various ways, when in fact a CPU emits heat other electromagnetic waves, which can be detected and from which inferences can be drawn, etc.
Canonical software development examples emphasizing “proving safety/usefulness before running” over the “tool” software development approach are cryptographic libraries and NASA space shuttle navigation.
At the time of writing this comment, there was recent furor over software called CryptoCat that didn’t provide enough warnings that it was not properly vetted by cryptographers and thus should have been assumed to be inherently insecure. Conventional wisdom and repeated warnings from the security community state that cryptography is extremely difficult to do properly and attempting to create your own may result in catastrophic results. A similar thought and development process goes into space shuttle code.
It seems that the FAI approach to “proving safety/usefulness” is more similar to the way cryptographic algorithms are developed than the (seemingly) much faster “tool” approach, which is more akin to web development where the stakes aren’t quite as high.
EDIT: I believe the “prove” approach still allows one to run snippets of code in isolation, but tends to shy away from running everything end-to-end until significant effort has gone into individual component testing.
The analogy with cryptography is an interesting one, because...
In cryptography, even after you’ve proven that a given encryption scheme is secure, and that proof has been centuply (100 times) checked by different researchers at different institutions, it might still end up being insecure, for many reasons.
Examples of reasons include:
The proof assumed mathematical integers/reals, of which computer integers/floating point numbers are just an approximation.
The proof assumed that the hardware the algorithm would be running on was reliable (e.g. a reliable source of randomness).
The proof assumed operations were mathematical abstractions and thus exist out of time, and thus neglected side channel attacks which measures how long a physical real world CPU took to execute a the algorithm in order to make inferences as to what the algorithm did (and thus recover the private keys).
The proof assumed the machine executing the algorithm was idealized in various ways, when in fact a CPU emits heat other electromagnetic waves, which can be detected and from which inferences can be drawn, etc.