[nickpsecurity]

So far, evidence is leaning toward latter view where physics imposes hard constraints on how we build our CPU's, etc for max performance. Same with software where certain things keep showing up (eg caching) due to mechanical constraints. Best result would seem to be a combo of abstract models for mathematical analysis and high-level languages that easily map to both those and the machines. Of course, many people have produced such tools. We're going in what appears to be objectively correct direction. :)

[pron]

Lamport also advocates abstract models and high-level specification, but in program logics (based on abstract state machines) rather than in programming languages.

[nickpsecurity]

That's what I said but in different words. That's slso been where the payoff has beenin about any, automated activity on software. Generally some math notation that's easy to analyze or something close to CPU/memory models.

Langsec is a notable exception where Chomsky's hierarchy paid off big time. The notations and implementations still more consistent with Lamport, though. So, semi-exception.