You write "These type-systems make sure that the code will not have errors at runtime." It should say that they make sure there won't be type errors at runtime. Many types of undesired behaviour ("errors") cannot be expressed and thus caught by a type system...
Thank you for the comment. It is difficult to express that some programming languages like Elm are not protected only from type runtime error but from all sorts of other errors. I rephrased it as:
These type-systems make sure that the code will not generate type errors at runtime. Moreover, together with other design choices, like making errors explicit in the type system ("Maybe", "Either", etc.), languages that use sound type-system are able to detect other families of runtime errors at compile time.
You write "These type-systems make sure that the code will not have errors at runtime." It should say that they make sure there won't be type errors at runtime. Many types of undesired behaviour ("errors") cannot be expressed and thus caught by a type system...
Thank you for the comment. It is difficult to express that some programming languages like Elm are not protected only from type runtime error but from all sorts of other errors. I rephrased it as:
These type-systems make sure that the code will not generate type errors at runtime. Moreover, together with other design choices, like making errors explicit in the type system ("Maybe", "Either", etc.), languages that use sound type-system are able to detect other families of runtime errors at compile time.
I hope it is clearer.
Yes, I love the clarity and explicitness of that! Happy Easter!