3 ms·
Exactly. E.g program analysis tools can tell you whether your code does not have bugs or it might have bugs (for a very large set of potential errors). For exa
by nextos 10y ago
Exactly. E.g program analysis tools can tell you whether your code does not have bugs or it might have bugs (for a very large set of potential errors).
For example, the Astrée static analyzer has checked the whole 100K LOC fly-by-wire Airbus software and determined there were only a few potential bugs amongst those classes of errors tested. That software was written in a Turing-complete C subset.
The key point to "get through" the halting problem in program analysis is to err on the safe side. That is, to allow false positives.
- seanmcdirmid 10y agoAll type systems have false positives by their nature. The trick is...humans have to be able to reason about their type errors so they can fix them. If the type system is too expressive, reasoning about type errors can be incredibly difficult. When I worked for coverity, a lot of time and resources were spent on consulting to help customers understand the errors they were getting, and to identify and lower false positives. Usability is key, or no one can/will use your stuff.