2 ms·
Rice's Theorem, as all Free Lunch Theorems, is too pessimistic. In real conditions, static analysis and theorem proving can verify lots of safety properties. S
by nextos 2y ago
Rice's Theorem, as all Free Lunch Theorems, is too pessimistic.
In real conditions, static analysis and theorem proving can verify lots of safety properties. See e.g. Astrée & Airbus, or F* and Project Everest.
IMHO, the solution is to use static analysis in conjunction with DSLs that have restricted semantics to make static analysis and hand-written proofs easy.
- samatman 2y agoIt doesn't appear that we're disagreeing. You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything it's supposed to. These are not the same thing in the general case. My actual point was that generic incompleteness and undecidability theorems do not guarantee that any given program must be defective. The thrust of langsec is in fact to parse all inputs at the boundaries, using algorithms with known properties, that is, ones where it's feasible to prove that they'll halt, won't overrun buffers, and so on.