> You have proved the original (deductive) claim "if it compiles, it works" for that one specific example, but that does not hold in general.

Are you sure it does not hold in general? Upon repeating mightybytes example with all Haskell functions vs another language I feel like you'd get similar results due to pervasive purity and the type system.