3 ms·

Theorem provers' type systems are not necessarily stronger than SML's or Haskell's; they are more expressive, which is a separate thing entirely. That said, yo

Theorem provers' type systems are not necessarily stronger than SML's or Haskell's; they are more expressive, which is a separate thing entirely. That said, your position is also just weird to me. Yes, theorem provers have nice type systems that are wonderfully expressive. The trade-off is that some common programming patterns become difficult to use or are even impossible. When it comes to everyday programming, I don't think theorem provers are at a point where they are particularly useful. Not everything needs to be proved formally, and I don't think this position is at odds with the belief that static type systems are generally "better" than dynamic ones.

ActorNightly 3y ago
> The trade-off is that some common programming patterns become difficult to use or are even impossible. Not really. Strong and expressive typing at its core is simply creating data packaging containers that have defined operations on them. It says nothing about logic. You may be referring to the functional programming aspect that comes with strong typed languages, which is related but not the same as strong typing. The point is that typing is just a tool that a programer can use, whether its built into the language or ran statically like MyPy. You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. However, in the case of strict+explicit typing, the idea is that you wouldn't need tests in the first place, because your code would be correct by nature of compilation.
- DonaldPShimoda 3y ago
  No, you are wrong. Some theorem provers, such as Coq, are not Turing-complete. This means you cannot write some programs, and in particular you cannot write infinite loops in Coq. Infinite loops are a common pattern (e.g., a REPL or a GUI display waiting for input). This is a trade-off, as I said. You gain the expressive type system, but lose the ability to implement certain programming patterns. It has nothing to do with the strength of the type system. --- > whether its built into the language or ran statically like MyPy. All (true) type-checking is static, so MyPy "running statically" is not a noteworthy feature to distinguish it from other type checkers. I guess this point may seem trivial to some, but the broader context of this conversation involves conflation of the terms "static type system" and "strong type system", so your misuse of the word "statically" here seems worth pointing out. That said, whether you use an external tool to check your types or the type-checker is built into the compiler is irrelevant, and I'm not sure why you brought it up at all. --- > You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. Depending on the perspective, this is factually incorrect. Type-checking is an ahead-of-time operation that guarantees the absence of certain classes of errors at run-time. Writing tests to check for the absence of such errors is not equivalent, because you have not proved anything; you merely gain confidence. They are semantically distinct, even if you write many tests to gain a lot of confidence.
  - ActorNightly 3y ago
    >Some theorem provers, such as Coq, are not Turing-complete. This means you cannot write some programs, and in particular you cannot write infinite loops in Coq. You are talking about languages, Im talking about the concept. The modern theorem provers aren't up to the task. Due to Rices theorem, you cannot "fully prove" a program, so a language that does this couldn't even exist. The strict typing however can be applied to subsets of the programming space, namely the data processing pipeline, whereas higher level stuff like the actual server code that does have an infinite loop to listen to requests can be written in whatever. The point is that no language recommended for strong type safety today is anywhere fully complete to include the rigor of something like a theorem prover, and anything less then that is basically your own opinion on what is "good enough". >Type-checking is an ahead-of-time operation that guarantees the absence of certain classes of errors at run-time. Run time errors are no different than compile time errors as far as testing is concerned. Its not like the computer blows up when you have a seg fault. And you absolutely can prove what you need for operation. Say your input to your code is an HTTP request of length x. And output is some data processing on that request. You can write a test suite that is basically like this 1. Ensure that code returns a well defined error for x values outside of given range. 2. For all valid ranges in x, test all possible values of every byte in that range, and ensure correct behaviour. While overkill, this will absolutely exercise every single piece of your code and prove correctness. You can also couple this with checking things like memory access

ActorNightly 3y ago

> The trade-off is that some common programming patterns become difficult to use or are even impossible. Not really. Strong and expressive typing at its core is simply creating data packaging containers that have defined operations on them. It says nothing about logic. You may be referring to the functional programming aspect that comes with strong typed languages, which is related but not the same as strong typing. The point is that typing is just a tool that a programer can use, whether its built into the language or ran statically like MyPy. You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. However, in the case of strict+explicit typing, the idea is that you wouldn't need tests in the first place, because your code would be correct by nature of compilation.

DonaldPShimoda 3y ago
No, you are wrong. Some theorem provers, such as Coq, are not Turing-complete. This means you cannot write some programs, and in particular you cannot write infinite loops in Coq. Infinite loops are a common pattern (e.g., a REPL or a GUI display waiting for input). This is a trade-off, as I said. You gain the expressive type system, but lose the ability to implement certain programming patterns. It has nothing to do with the strength of the type system. --- > whether its built into the language or ran statically like MyPy. All (true) type-checking is static, so MyPy "running statically" is not a noteworthy feature to distinguish it from other type checkers. I guess this point may seem trivial to some, but the broader context of this conversation involves conflation of the terms "static type system" and "strong type system", so your misuse of the word "statically" here seems worth pointing out. That said, whether you use an external tool to check your types or the type-checker is built into the compiler is irrelevant, and I'm not sure why you brought it up at all. --- > You can take a piece of code in C, and write a test suite on input and output of that piece of code, and accomplish much of the same thing that typing accomplishes. Depending on the perspective, this is factually incorrect. Type-checking is an ahead-of-time operation that guarantees the absence of certain classes of errors at run-time. Writing tests to check for the absence of such errors is not equivalent, because you have not proved anything; you merely gain confidence. They are semantically distinct, even if you write many tests to gain a lot of confidence.
- ActorNightly 3y ago
  >Some theorem provers, such as Coq, are not Turing-complete. This means you cannot write some programs, and in particular you cannot write infinite loops in Coq. You are talking about languages, Im talking about the concept. The modern theorem provers aren't up to the task. Due to Rices theorem, you cannot "fully prove" a program, so a language that does this couldn't even exist. The strict typing however can be applied to subsets of the programming space, namely the data processing pipeline, whereas higher level stuff like the actual server code that does have an infinite loop to listen to requests can be written in whatever. The point is that no language recommended for strong type safety today is anywhere fully complete to include the rigor of something like a theorem prover, and anything less then that is basically your own opinion on what is "good enough". >Type-checking is an ahead-of-time operation that guarantees the absence of certain classes of errors at run-time. Run time errors are no different than compile time errors as far as testing is concerned. Its not like the computer blows up when you have a seg fault. And you absolutely can prove what you need for operation. Say your input to your code is an HTTP request of length x. And output is some data processing on that request. You can write a test suite that is basically like this 1. Ensure that code returns a well defined error for x values outside of given range. 2. For all valid ranges in x, test all possible values of every byte in that range, and ensure correct behaviour. While overkill, this will absolutely exercise every single piece of your code and prove correctness. You can also couple this with checking things like memory access