inet-os

A whole operating system can run on top of interaction nets.

We only need a few primitives to do this.

Limits

Redexes would have a provenance that points to a limit object. It determines the max amount of rwts/mem/limits that a set of redexes can use before stopping.

// Id is the type of λx x
HVM.max_rewrites: (max: u64) -> (f: (Id -> U)) -> Either (Id -> U) U
HVM.max_nodes: (max: u64) -> (f: (Id -> U)) -> Either (Id -> U) U
HVM.max_limits: (max: u64) -> (f: (Id -> U)) -> Either (Id -> U) U

// Provenance/Program internal state:
struct State {
  rewrites: u64,
  nodes: u64,
  limits: u64,
}

This would allow running untrusted code.

IO

Continuation passing style would be used to carry out IO.