I haven’t entirely followed what you meant by a solution to IO, but I’m not to surprising to hear there’s a solution.

I guess the point I had in mind was, in making the case of dependent languages stuff like this may not be immediately apparent (I might be confusing the concept of total languages or programming which may not necessarily be coupled to dependent types).

> as an aside by IO I do mean anything not known at compile time (interrupts & user input, network responses, network requests [who API may change in a breaking way], database entries, etc)

Cheers for your insight btw