You're right, of course, that systems security encompasses more than a formally-verified system can encompass. I say this having worked for a group that pitched

You're right, of course, that systems security encompasses more than a formally-verified system can encompass. I say this having worked for a group that pitched the DoD and private vendors on "provably correct" systems that relied on commodity operating systems and compilers, so I really do get it, and know just how horribly limited formal methods are in the real world. My point is, as I originally suggested, that any static analysis would likely be an improvement over what currently happens in the LAMP world. Most compiled languages have at least some tools available which developers can use to perform basic sanity checks -- the compiler itself being of course the first and most oft-overlooked of these. Dynamic language users lack even that basic safety net, which is the reason for my primary argument about the benefits of type safety and static analysis. Basically, we're in furious agreement, and if you had caught me at a different time of day or mood, I could just as easily be standing on your side of the fence, arguing against someone who was trying to tell me that theory could solve all my security problems.