[rmcclellan]

I agree with the sentiment that the problem the OP brings up is difficult, but bringing up the halting problem here seems pretty pedantic.

If you restrict yourself to a turing incomplete language, checking a specification no longer reduces to the halting problem. In fact, there are many systems that do exactly this, and most of these systems are perfectly capable of sorting a list and proving that the list is sorted.

However, I think the real point is that there are at least dozens of smart people who are working on this exact problem all day, every day. The OP shows neither a deep understanding of why previous attempts at this have failed or really, any knowledge at all about the state of the field of programming language research.

[dullcrisp]

Can you provide links to papers which try address this problem in practical terms, or some leads that one might use to acquaint themselves on the current state of research in this area? The paper the parent links I've only skimmed but what it seems to be advocating seems not to be that far from test-driven development. Has anyone tried anything more closely resembling what the OP is proposing? Are any such attempts doomed fromt he start?

[jng]

You are right, I'm not intimately familiar with all the research out there and with all the details. I do think I have some useful things to add, that a "practical" angle is missing in many approaches, and that many attempts fail just because they get lost in trying to achieve theoretically elegant solutions, rather than building practical tools.

At least, I'll learn a lot. At most, we get something new with the help of other people.