Incorrect. Static typing can prove many things, depending on the quality of the type system.
At the very least, it proves that your data is organized, stored, passed around and used in a logically valid and consistent manner. Make that proof impossible, and the compiler complains. (And with good reason - it doesn’t matter how good your program logic is if you’re feeding it bad data. Garbage in, garbage - or a runtime error - out.)
In a dynamically typed language, your program logic still implicitly depends on that proof holding - it’s just that you, the fallible human, has to make sure everything checks out. Python added type hints for precisely this reason.
Additionally, with more advanced static type systems, it becomes possible to issue guarantees beyond simple type safety. Patterns like typestate (found in TS, Haskell and Rust, off the top of my head) can be used to make illegal states unrepresentable at compile time. Try to write to a closed file or make an invalid state machine transition? The compiler will see it and say no.
It just creates bugs and crashes.
In what universe are runtime errors turned compile-time errors a source of bugs and crashes? A statically-typed program won’t blow up in production because some poor intern wasn’t able to keep the implicit type bounds of every single function parameter in his head.
There’s some math & CS papers you should read, Gödel’s incompleteness theorem, Turing’s halting problem. YOU CANNOT prove your way out of logic errors. You cannot make a universal type system. All you’re doing is wasting time with false confidence.
Typing can’t prove anything, either. It just creates bugs and crashes.
Your program logic is the part that will not be fixed by it.
Incorrect. Static typing can prove many things, depending on the quality of the type system.
At the very least, it proves that your data is organized, stored, passed around and used in a logically valid and consistent manner. Make that proof impossible, and the compiler complains. (And with good reason - it doesn’t matter how good your program logic is if you’re feeding it bad data. Garbage in, garbage - or a runtime error - out.)
In a dynamically typed language, your program logic still implicitly depends on that proof holding - it’s just that you, the fallible human, has to make sure everything checks out. Python added type hints for precisely this reason.
Additionally, with more advanced static type systems, it becomes possible to issue guarantees beyond simple type safety. Patterns like typestate (found in TS, Haskell and Rust, off the top of my head) can be used to make illegal states unrepresentable at compile time. Try to write to a closed file or make an invalid state machine transition? The compiler will see it and say no.
In what universe are runtime errors turned compile-time errors a source of bugs and crashes? A statically-typed program won’t blow up in production because some poor intern wasn’t able to keep the implicit type bounds of every single function parameter in his head.
There’s some math & CS papers you should read, Gödel’s incompleteness theorem, Turing’s halting problem. YOU CANNOT prove your way out of logic errors. You cannot make a universal type system. All you’re doing is wasting time with false confidence.
I never said that static typing stops all logic errors or fully proves program correctness, but go off I guess…