The assert() statement is excellent, and provides a reasonable first-step in what I'm trying to describe, here.
That it's largely unused is something that needs to be tackled, but one impossible mission at a time. :)

What I'm looking for is something that will determine if the -meaning- of a function is correct, not just the syntax. If you were looking at the assert() function, it would be the same as the compiler running a bunch of test cases against the assert()s, to see if they were logically consistant -and- that, for EACH function, assuming the initial assert() holds true, will the assert() at the end of that function be necessarily true.

This is difficult, but not impossible, to do. Let's say your initial assert() states that x > 1, and your function reduces x by 1. A final assertion of x > 0 is necessarily true. A final assertion of x <y, where y is any number less than 0 is necessarily false. A final assertion of x> y, where y is any number greater than 0 is potentially false, and (if you want strict checking) should be treated as if necessarily false.

Ok, so how do you do this, without clogging up the machine by testing every possible value, and seeing if it ends up invalid?

Well, there are short-cuts. If you want the compiler to also do test runs, it at most needs to run through four cases for every function that can be reversed. (Take the minimum and maximum values of the pre- and post-conditions, and run the code forwards or backwards, then see if the values still lie within bounds.)

For more complex functions, you'd need to be a bit more crafty. You need to describe the function in abstract terms, collect operations dealing with the same data as far as possible without changing what the program does, simplify, and test each block of what's left, as above. (This would bloat the compiler something chronic, but if the resultant code was better, it might be worth it.)

PLEASE NOTE: You can't sort all code, all the time. Let's say you have the code:

y += 1;

x += 1;

y += 1;

if (x > y) do_something();

x += 1;

Now, the two y += 1's -can- be combined, because there is nothing dependent on y between those two statements. The two x += 1's cannot, because there is an intermediate dependency, the if.

Now, y += 2 will meet the same assertions, at the start and end, as two y += 1's.

If you want to be even smarter about it, then you would take the initial assertion, and concatinate operations onto it. If the resulting expression is functionally identical to the last assertion, then the code is correct.

This is harder, because what you're doing involves being able to simplify equations, collect terms, and generally do the stuff some of the better maths packages do, only for potentially horrible equations, and multiple variables.

This is the same as running the 4 cases, in lots of ways, except that you don't have this nagging "what if..." - what if some other value hits a discontinuity in the maths or logic? what if the results are horribly non-linear, so taking the extremes -doesn't- give an indication of how the rest of the values will behave?

By showing that your initial assertion, plus your function, equals your final assertion, for each path through that function, you're assured that if anything is incorrect, it is at least incorrect in a predictable way, and to the coder's specification.

Now for the REALLY complicated part - something that'll handle low-level operations. Here, we can make use of the fact that we are moving more and more towards validating the function, rather than the form. A low-level operation (such as calling a function via a pointer) really doesn't matter, provided we know what's passed in, what's returned and that the called function doesn't try to manipulate anything outside of its scope. (When you get side-effects in a program, ALL bets are off. You can't check it, because you have no means of knowing what to check.)

So, what we're doing, here, is to say that read-only parameters are going to be unchanged, and that read-write parameters AND any return value can have any value that is valid for that type. If it's a function within the program, you can also assume that the value(s) will comply with the post-condition.