Yep, this is the case: the type-checker allows arbitrary computation to occur at compilation time. You can see some of that here, where I've implemented peano a

Yep, this is the case: the type-checker allows arbitrary computation to occur at compilation time. You can see some of that here, where I've implemented peano arithmetic/addition/multiplication/branching using the type system: https://github.com/zesterer/tao/blob/master/examples/type-astronomy.tao https://github.com/zesterer/tao/blob/master/examples/type-as... . I've not yet had the time or mental fortitude to implement something more non-trivial like N-queens or a Brainfuck interpreter, but perhaps eventually!