With respect, I disagree. Specification and design/implementation are not separate concerns. They are dual. A sufficiently detailed specification is an implem

With respect, I disagree. Specification and design/implementation are not separate concerns. They are dual. A sufficiently detailed specification is an implementation. Prolog does this (and Eve has a very similar feel). As engineers, we traditionally work declaratively at the top of the "V" and imperatively at the bottom of the "V" -- but the reasons for this are largely historical/cultural. We could (in theory) carry out the analysis/refinement process using entirely declarative notation. The problem domain has primacy. Analysis separates problem-domain concerns and the duality takes care of the translation between problem and solution domains. (OK -- so this is basically just a reiteration of the thesis of good old-fashioned AI -- that with a sufficiently powerful theorem prover and a sufficiently large and detailed knowledge base -- solutions will just pop out of a largely mechanical analysis process -- and I'm pretty sure this isn't at all trendy right now ... so I should relegate this to the "thinking out loud" bucket ...)