Name: Anonymous 2013-12-28 4:57
What kinds of static code analyses has humanity implemented over the years? Which of them turned out to be the most practically useful?
We know that the common System F-ish type systems are tractable but not really useful for error detection.
Dependent types are more powerful but they seem to be too unwieldy for practice (nobody's really embracing them for programming despite the fact they've been around for decades).
Contracts are practical but they're just runtime asserts, no static analysis.
Perhaps, SMTs are the future? Have you ever used them for your projects?
Then there are variable lifetime analyses, region typing for safe storage management... there's so much stuff but nothing makes it to the industry. When Haskell's primitive System F-like type system is a beacon of static safety, something's clearly wrong about the state of the world. Or maybe it's the whole idea of static code analysis that's wrong and useless for real life?
We know that the common System F-ish type systems are tractable but not really useful for error detection.
Dependent types are more powerful but they seem to be too unwieldy for practice (nobody's really embracing them for programming despite the fact they've been around for decades).
Contracts are practical but they're just runtime asserts, no static analysis.
Perhaps, SMTs are the future? Have you ever used them for your projects?
Then there are variable lifetime analyses, region typing for safe storage management... there's so much stuff but nothing makes it to the industry. When Haskell's primitive System F-like type system is a beacon of static safety, something's clearly wrong about the state of the world. Or maybe it's the whole idea of static code analysis that's wrong and useless for real life?