3 ms·

> There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs,

> There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones. Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.

draw_down 8y ago
The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
- seanwilson 8y ago
  > The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry. Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris). I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
- giornogiovanna 8y ago
  The simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious. [0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
aassddffasdf 8y ago
Property-based tests do this at runtime too (and they catch far more bugs than you'd imagine going into it).
- seanwilson 8y ago
  Property-based tests are really practical and will find bugs unit tests don't, but type checking is an exhaustive proof that the properties you've expressed with types hold for all inputs/outputs. A key point though is the type systems of most mainstream languages don't let you express complex program properties (e.g. the input list must be sorted), so your only option is to use unit tests or similar to check those.
  - aassddffasdf 8y ago
    Yes, I know that. However, they don't need to be exhaustive. They are very effective at uncovering any bugs using a statistical approach at even very reasonable levels of iteration. And nothing precludes you from running them 24/7 in the cloud. I wouldn't say using a "unit test" is ever really a viable option for me. Property-based tests subsume unit tests.
slaymaker1907 8y ago
There is a problem though that Turing completeness allows for inconsistencies. i.e., you can technically "return" a bottom type in these languages by looping forever. That is actually why Coq is not Turing complete since Coq is primarily used for theorem proving and less for programming.
- lapinot 8y ago
  Turing completeness as the ultimate measure of expressiveness for programing/logical systems is a myth. I argue every interesting program you may want to write is either terminating, co-terminating or step-indexed. Terminating programs are well understood (using structural recursion, inductive data, etc). Co-terminating programs are stuff like servers/daemons/guis: you want them to (possibly) never terminate and always progress (respond) in finite time, these are expressible using coinductive data, structural corecursion etc. And lastly, if you have a program which may hang for an indefinite amount of time, you really should put a timeout (or heck, a co-timeout, eg some kind of heartbeat), that's step-indexing. So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time. See this paper for some more insights: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....

draw_down 8y ago

The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.

seanwilson 8y ago
> The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry. Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris). I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
giornogiovanna 8y ago
The simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious. [0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...

aassddffasdf 8y ago

Property-based tests do this at runtime too (and they catch far more bugs than you'd imagine going into it).

seanwilson 8y ago
Property-based tests are really practical and will find bugs unit tests don't, but type checking is an exhaustive proof that the properties you've expressed with types hold for all inputs/outputs. A key point though is the type systems of most mainstream languages don't let you express complex program properties (e.g. the input list must be sorted), so your only option is to use unit tests or similar to check those.
- aassddffasdf 8y ago
  Yes, I know that. However, they don't need to be exhaustive. They are very effective at uncovering any bugs using a statistical approach at even very reasonable levels of iteration. And nothing precludes you from running them 24/7 in the cloud. I wouldn't say using a "unit test" is ever really a viable option for me. Property-based tests subsume unit tests.

slaymaker1907 8y ago

There is a problem though that Turing completeness allows for inconsistencies. i.e., you can technically "return" a bottom type in these languages by looping forever. That is actually why Coq is not Turing complete since Coq is primarily used for theorem proving and less for programming.

lapinot 8y ago
Turing completeness as the ultimate measure of expressiveness for programing/logical systems is a myth. I argue every interesting program you may want to write is either terminating, co-terminating or step-indexed. Terminating programs are well understood (using structural recursion, inductive data, etc). Co-terminating programs are stuff like servers/daemons/guis: you want them to (possibly) never terminate and always progress (respond) in finite time, these are expressible using coinductive data, structural corecursion etc. And lastly, if you have a program which may hang for an indefinite amount of time, you really should put a timeout (or heck, a co-timeout, eg some kind of heartbeat), that's step-indexing. So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time. See this paper for some more insights: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....