3 ms·

This is really exciting. I am an absolute beginner at TLA+ but I really like this possible design space. I have an idea for a package manager that combines ty

This is really exciting. I am an absolute beginner at TLA+ but I really like this possible design space. I have an idea for a package manager that combines type system with this style of deterministic testing and state space exploration. Imagine knowing that your invocation of package-manager install <tool name> Will always work because file system and OS state are part of the deterministic model. or an next gen Helm with type system and state space exploration is tested: kubectl apply <yaml> will always work when it comes up because all configuration state space exploration has been tested thanks to types.

__MatrixMan__ 3y ago
Coincidence, I'm reading this and thinking about test harnesses for my package manager idea, which is really just a thin wrapper around nix, designed under the assumption that the network might partition at any moment: keep the data nearest where it's needed, refer by hash not by name, gossip metadata necessary to find the hash for you, no single points of failure. Tell me more about yours?
- samsquire 3y ago
  I am thinking about state machine progressions and TLA+ style specifications which are invariants over a progression of variables. Your package manager knows your operating system's current state and the state space of all the control flow graph through the program and configuration together can go to, it can verify that everything lines up and there will be no error when executed a bit like a compiler but without causing the Halting problem. In TLA+ you can dump a state graph as a dot file, which I turn into a SVG and run with TLA+ graph visualiser. Types verify possible control flow is valid at every point. We just need to add types to the operating system and file system and represent state space for deterministic verification. You could hide packages that won't work. The package manager would have to lookup precached state spaces or download them as part of the verification process.

__MatrixMan__ 3y ago

Coincidence, I'm reading this and thinking about test harnesses for my package manager idea, which is really just a thin wrapper around nix, designed under the assumption that the network might partition at any moment: keep the data nearest where it's needed, refer by hash not by name, gossip metadata necessary to find the hash for you, no single points of failure. Tell me more about yours?

samsquire 3y ago
I am thinking about state machine progressions and TLA+ style specifications which are invariants over a progression of variables. Your package manager knows your operating system's current state and the state space of all the control flow graph through the program and configuration together can go to, it can verify that everything lines up and there will be no error when executed a bit like a compiler but without causing the Halting problem. In TLA+ you can dump a state graph as a dot file, which I turn into a SVG and run with TLA+ graph visualiser. Types verify possible control flow is valid at every point. We just need to add types to the operating system and file system and represent state space for deterministic verification. You could hide packages that won't work. The package manager would have to lookup precached state spaces or download them as part of the verification process.