I think the people that say we don't need Turing completeness say that because their models can't really accommodate proper reasoning about exactly the kinds of systems I want to reason about. Proving theorems is nice and all but at the end of the day the temporal and dynamic aspects of the system I'm building are what I really care about. Not some static snapshot of it but the actual evolving gestalt.
Oh, absolutely, but there are formal methods for working with that, too -- well, maybe just the "evolving" part if not the "gestalt" -- mostly based on temporal logic (I can't believe I'm arguing on the side of formal methods now...) See, e.g. the Esterel language[1] used in the industry (directly or through its descendent languages) to write full, safety critical real-time systems. It is an imperative, non-Turing complete language, that is fully verifiable, and actually able to track an evolving gestalt for some restricted definition of "gestalt". Esterel, BTW, has had much more success than Haskell in the industry.
Another example is TLA+, which is used by Amazon to verify their (Java, I assume) web services[2]. Unlike Esterel, TLA+ is Turing complete, and can therefore fail to prove many things. It will also take longer and longer to run the bigger the code is, and therefore only verify algorithms, not entire systems.
Also, see the history of Statecharts[3], a predecessor to Esterel, that was designed first and foremost to assist humans in writing specifications and only later combined with Pnueli's temporal logic to facilitate formal methods.
BTW, the same David Harel who worked with Pnueli on Statecharts and temporal logic, is now involved with Behavioral Programming[4] a very interesting programming style that makes human specifications easier to translate to code. For a usage example, see Harel et al., Programming Coordinated Behavior in Java[5]
