[pron]

While not exactly a debate -- more of a fundamental difference in outlook -- these are interesting, completely opposite claims:

Bob Harper[1]:

> There is an alternative… without… reference to an underlying machine… [W]e adopt a linguistic model of computation, rather than a machine model, and life gets better! There is a wider range of options for expressing algorithms, and we simplify the story of how algorithms are to be analyzed.

Leslie Lamport[2]:

> Thinking is not the ability to manipulate language; it’s the ability to manipulate concepts. Computer science should be about concepts, not languages. … State machines… provide a uniform way to describe computation with simple mathematics. The obsession with language is a strong obstacle to any attempt at unifying different parts of computer science.

[1]: https://existentialtype.wordpress.com/2011/03/16/languages-a...

[2]: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...

[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.

[agumonkey]

pardon my anecdote but after years of imperative and OOP, ad nauseam, I went into LISP/ML, to be stateless, but then structural parametric types and "state" got closer and closer at the conceptual level, just not "mutable".