> Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem.

Not even close. Compiling cannot even check if your program computes 2+2 correctly, much less anything more complicated (e.g. calculating tax values for a service provided based on, you guessed it, runtime lookups because taxes can and will change).

Compiling with static typing will indeed check that your functions are called with correct input values (for some value of correct) across your codebase.