I think that the term “incorrectly typed function” is not very useful in Julia. AFAIK it is considered best practice to use function signatures only for dispatch, and not for safety or other motivations of restricting.
The language is dynamic, thus certain problems manifest only at runtime. This is by design. Moreover, there is no separate compile time in Julia, code generation is just intermezzo of execution. “Only fails at runtime” is something most of us stop saying after a few months of working with Julia.
Yes, static analysis of the language is relatively hard, especially when you compare it to less dynamic languages. This is a sad result of runtime code generation, which is one major selling point of Julia. I hope that tooling will help more in the future.
Yes, proving correctness in Julia is even harder than in other languages. I personally think that proving correctness of nontrivial programs requires special languages and tooling, and is futile in any general-purpose language, so I don’t feel this a problem.
Please also note that structural subtyping is not a feature of Julia, at least in my understanding. Duck typing is.