Generally, refactoring in dynamic languages without tests or something like Clojure's schema is madness. Usually not a problem in strongly typed languages, even without much test coverage.
A subset which has nothing to do with, for instance, the corretness of loops. Because type checking doesn't verify those. Well typed doesn't even tell you whether a program terminates or not and on what inputs.
A program that is supposed to calculate pi could calculate e instead, yet be well typed (everything is a double-precision float, or a function from several of them to one, check!)
On the contrary, knowing that a piece of lambda calculus can be simply typed tells me for certain that the program halts for all inputs.
If you demand it work for arbitrary programs, then sure, well typed doesn't "even" tell you that. But no procedure can "even" tell you that (including, probably, anything that can be done by our brains), so it's a rather odd choice as a low-bar.
If you really wanted, you could derive a proof that pi is equivalent to some sort of corecursive series, which you can then evaluate in a dependently typed language, I guess. A proof is a type.
On the other hand, how would you write a unit test that checks whether something calculates pi without comparing its result to pi itself?
> A proof is a type.
Yes, Curry-Howard and all that.
If I just write a well-typed function which supposedly calculates pi, the rather trivial well-typedness is not informative by itself.
You're talking about adding reams of verbiage requiring expertise in using an advanced type system for executing a proof.
This isn't how static type systems are actually used and advocated in the field, and it is not feasible in general, only for toy, academic examples.
The proof code, which will exceed the size of the original function by at least an order of magnitude, could also be buggy. At the end of the day, it's just more code.
It reminds me of the argument fropm the Lisp camp: "Well, I could just write (supermacro ...) which implements any syntax and semantics whatsoever". (No, in fact you can't, and the proof is that you never actually will.)
What does it mean? It means 35% of the code is being refactored without coverage. Its status is "unknown" before refactoring and "unknown" after.
Oh, but it compiles!