That’s pure nonsense. Types don’t tell you that your code is correct, they just tell you that your types align. Here’s a perfect example of where the mentality that if it compiles, ship it leads you in practice.
Haskell bro wrote a benchmark comparing Haskell with C implementation of websockets. The initial results looked extremely favorable for Haskell. However, it turned out that the Haskell implementation failed to deliver messages reliably, dropping 98% of the messages it received.
Furthermore, static typing is that it’s inherently more limiting in terms of expressiveness because you’re limited to a set of statements that can be verified by the type checker effectively. This is a subset of all valid statements that you’re allowed to make in a dynamic language.
So, a static language will often force you to write code for the benefit of the type checker as opposed to the human reader because you have to write code in a way that the type checker can understand. This can lead to code that’s more difficult to reason about, and you end up with logic errors that are much harder to debug than simple type mismatches. People can also get a false sense of confidence from their type system as seen here where the author assumed the code was correct because it compiled, but in fact it wasn’t doing anything useful.
At the same time, there is no automated way to check the type definitions themselves and as you encode more constraints via types you end up with a meta program describing your program, and there is nothing to help you know whether that program itself is correct. Consider a fully typed insertion sort in Idris. It’s nearly 300 lines long! I could understand a 10 line Python version in its entirety and be able to guarantee that it works as intended much easier than the Idris one.
deleted by creator
Because if the types are correct, it’s mostly bug free already, right?
deleted by creator
That’s pure nonsense. Types don’t tell you that your code is correct, they just tell you that your types align. Here’s a perfect example of where the mentality that if it compiles, ship it leads you in practice.
Haskell bro wrote a benchmark comparing Haskell with C implementation of websockets. The initial results looked extremely favorable for Haskell. However, it turned out that the Haskell implementation failed to deliver messages reliably, dropping 98% of the messages it received.
Furthermore, static typing is that it’s inherently more limiting in terms of expressiveness because you’re limited to a set of statements that can be verified by the type checker effectively. This is a subset of all valid statements that you’re allowed to make in a dynamic language.
So, a static language will often force you to write code for the benefit of the type checker as opposed to the human reader because you have to write code in a way that the type checker can understand. This can lead to code that’s more difficult to reason about, and you end up with logic errors that are much harder to debug than simple type mismatches. People can also get a false sense of confidence from their type system as seen here where the author assumed the code was correct because it compiled, but in fact it wasn’t doing anything useful.
At the same time, there is no automated way to check the type definitions themselves and as you encode more constraints via types you end up with a meta program describing your program, and there is nothing to help you know whether that program itself is correct. Consider a fully typed insertion sort in Idris. It’s nearly 300 lines long! I could understand a 10 line Python version in its entirety and be able to guarantee that it works as intended much easier than the Idris one.