Comment by samsquire | Hacker News Reader

Comment by samsquire | Hacker News Reader

Parent Full thread

This is very interesting and could lead to some futuristic programming technology.

I kind of want to plot the state space of a program to see all available states.

In my exploration of distributed systems, microservices and multithreaded systems, it is extremely helpful to try and see what potential states the system can be in. Global and local reasoning of these kinds of software is rather difficult.

I've written about value tracing but I've not heard of treating values as types. I would love to be able to see the trajectory of a value through different states - such as membership to different collections. For example, if you have different collections or sets and items are removed from one collection and added to the other.

https://github.com/samsquire/ideas4#571-value-calculus-varia...

I've never written a TLA+ specification and I'm a complete beginner to this space but I've been trying to understand the dining philosophers one. TLA+ Toolbox is aware of discrete states in the state space, which is absolutely awesome. Types can inform us about future possible valid states.

I began writing a visualisation of memory and animated the movement of memory around to try reveal patterns. If you think of memory as state space, you can see movements of memory as picking things up and putting them down.

https://replit.com/@Chronological/ProgrammingRTS#index.html

If we see types or values as positions, we can create animations of the state space unfolding in front of us. This is the dream.

(My plan is to write a programming simulation that is controlled similar to a real time strategy game as an alternative form of programming)

> 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.

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

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.

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.

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.

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

Reply on news.ycombinator.com