[l_dopa]

That's a very strange interpretation of Rice's theorem. Just because properties of computable functions are undecidable doesn't mean they somehow "can't be described by mathematics". I'm also not sure why incompleteness is relevant here at all, unless you think describing something mathematically requires a complete formal system. In that case, we can't "describe" arithmetic "mathematically".

[eli_gottlieb]

It's not that strange. We can write all kinds of program analyses that are decidable, but which are necessarily conservative, and we end up deciding what sort of conservativeness (which side we want to err on) in different situations. What this does mean is that you can't really write a Grand Unified Formal Verification framework and get some wonder-of-wonders benefit just by switching to functional programming.

I've also spent enough time around Haskell coders to notice that the instant you give them a fresh new language feature, they will push it right out to the limits where the compiler's conservative analyses no longer work and the programmer has to manually assert that the code is correct.

Nothing will really save the programmer from having to think clearly about their own code, and most language features designed to ostensibly help do so just enable compiler-abuse at a higher level of abstraction.