Implementing Pure Functions

[bearophile]

Walter:

> I've tried out the theorem prover in Spec#. It only works in trivial cases.

You are beating this horse a bit too much.
It uses a quite refined theorem prover, it works, but as I have said from the beginning it doesn't work in all cases. There are always cases automatic provers aren't able to handle. The case you have found is hard. Have you sent them a bug report?
Even the one of SPARK doesn't work in all cases. When the one of SPARK doesn't work, then the programmer has to write down the proof manually (or half-manually, with an interactive prover).

Bye,
bearophile