Some languages can detect this at compile time. For example, ATS - a dependently typed language:

   fun square {m:int} (a: int m): int (m*m) = a + 2

This won't compile because in the type we've said the result must be the square of the input. I've written some more about using dependent types [1] and proofs [2,3] for this sort of thing.

The difference between writing proofs and writing tests is subtle though and serve similar purposes. Tests can make you feel confident that things are right but proofs should make you certain of it.

[1] http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h... [2] http://bluishcoder.co.nz/2013/07/01/constructing-proofs-with... [3] http://bluishcoder.co.nz/2012/10/04/implementing-a-stack-wit...