Hacker News new | ask | show | jobs
by greenfield1 1137 days ago
> I kind of want to plot the state space of a program to see all available states.

In the ideal program, only legal states are reachable. If you can use your type system to prevent to ever run into an illegal state, then you have won quite a lot. This is basically the holy grail of programming. Not sure we'll ever get there though.
1 comments
scns 1137 days ago
With strong type system a la ML (OCaml, Haskell, F#, Rust, Elm etc) it is allready possible, am i wrong?

https://www.youtube.com/watch?v=IcgmSRJHu_8

link
kaba0 1137 days ago
It is not possible, normal types can only prove so-called trivial properties (from Rice’s theorem). Every non-trivial property is unprovable in the general case.

Dependent-type systems can express more things (e.g. they can represent a concat function that takes two lists of n and m length, and return a list of length n+m), but proving those properties are hard and may not scale well. There are trade offs, like one might not have to actually prove the properties, just having them as facts may also be good enough.

link
UncleMeat 1136 days ago
Types can only decide trivial properties. But that's fine. We can accept false positives (valid programs that nevertheless type incorrectly and are rejected by the compiler). You still get very powerful reasoning with this.

Dependent types are also equally stymied by Rice's Thm. Both are static techniques. Path based type reasoning doesn't do anything to solve the halting problem. It just means more expressive types.

link
greenfield1 1137 days ago
I doubt it. The ultimate consequence of this endeavour is that a program that takes an int as input and produces an int as output would then have the type a:A->B(a). For example, a program P that for a given n produces the n-th prime number would express this in its type signature. Another program using that as a sub-function and doing p=P(n) could never reach the state where p is not the n-th prime number, the type system would be able to express that, and the type checker would need to be able to validate it. Etc. etc.

A type checker would amount to an automatic correctness proof, which in its full generality is impossible (by halting problem), but for the practically interesting classes could be done using a theorem prover / proof assistant and the occasional hint from the programmer. That would be great to have, but none of the examples you mention is anywhere close.

link
kaba0 1137 days ago
Dependent types are this basically, Idris, Lean, etc having it. Though proving is a huge challenge, so it is no panacea.
link