To continue the thought: This dependent type is expressible, trivially decidable, and has no additional side effect burden:

"This function's type depends on its function name. If its function name is "sqrt", then {check some simple rules about square roots, like if x is 0 then output is 0, if x > 1 then output < x, etc.}"

This one too:

"This function's type depends on its function name. If its function name is "sqrt", then check that it calls and returns a formally verified square root function applicable to its input type that is known to be decidable and appropriate to the floating point math definitions we're operating in right now"