> maybe some combination of static analysis and testing can make sure my implementation matches it?
I'm becoming a fan of the ideas espoused in eg http://www.vpri.org/pdf/m2009001_prog_as.pdf and http://shaffner.us/cs/papers/tarpit.pdf where rather than trying to verify that arbitrary code matches your specification, you make the specification itself executable and then supply hints and heuristics on the most efficient way to execute it. It's a similar idea to first writing an sql query and then hinting which execution plan should be used. Compared to writing arbitrary code this approach limits expressiveness but it removes the verification problem entirely. So far we've only seen this approach used heavily in querying and in constraint solving. Luckily, it turns out that large chunks of the programs we write day to day can be expressed in terms of either database-style queries or constrained search (see eg http://boom.cs.berkeley.edu/).
I think that in the medium term, this is a good place to go. Specify denotation, and operational constraints, and then fill in details whenever the compiler can't figure out the rest.
Actually, the above is how I've been thinking about it for a while, but I'm not sure there's any reason we can't say "denotational constraints" as well - where exact denotation is just a particularly tight constraint.
I'm becoming a fan of the ideas espoused in eg http://www.vpri.org/pdf/m2009001_prog_as.pdf and http://shaffner.us/cs/papers/tarpit.pdf where rather than trying to verify that arbitrary code matches your specification, you make the specification itself executable and then supply hints and heuristics on the most efficient way to execute it. It's a similar idea to first writing an sql query and then hinting which execution plan should be used. Compared to writing arbitrary code this approach limits expressiveness but it removes the verification problem entirely. So far we've only seen this approach used heavily in querying and in constraint solving. Luckily, it turns out that large chunks of the programs we write day to day can be expressed in terms of either database-style queries or constrained search (see eg http://boom.cs.berkeley.edu/).