> The size of the verifier and runtime is absolutely relevant to keeping the TCB down to a manageable level.

Sure, but that's not the point I was making. The missing instructions are largely polymorphic operations on various integral and floating point types. WASM verification is not as hard as you seem to be implying.

> The register allocation is done by the untrusted code and is only verified by the runtime. You can still achieve very good register usage.

There are ways to do this safely even in stack machines. See: http://lambda-the-ultimate.org/node/5375

> WASM is a stack based machine which means you have a strict choice between fast JITed and a dead simple code generator.

A dead simple code generator that can only make use of 10 registers isn't all that compelling. Stack machines are great for compact code, and subexpression elimination and register allocation makes stack machines largely competitive with register machines. A lot of this can be moved offline as well (see link above).

> The two address register instruction part that you cut off is an extremely important part of that.

2-address instructions aren't competitive on all archs. They lead to unnecessary move sequences on 3-address architectures for one. This is why register allocation belongs in the VM.

> It's tractable because the code flow graph is a DAG with non infinite code size. The macro example doesn't apply because there's no in kernel expansion like that.

"DAG with non-infinite code size" also describes CPP, which is why I brought it up. That property simply doesn't say much.

> It's only been done for Turing complete languages by keeping to a Turing incomplete subset. That's how sel4 works for instance.

Not true, it's been done for SML with region-based memory management (MLKit IIRC). Regions with lexical lifetimes are just folded into the stack, but there's no requirement to restrict yourself to a Turing incomplete fragment (although your program must terminate, obviously, but that isn't the same thing).

> Limiting expressiveness is the only way to get to verification. That's a natural consequence of the Halting problem.

There are various ways to restrict programs though, so you don't have to restrict a language at the syntactic level which is far more painful than alternatives. For instance, sized types to guarantee termination and estimate space use.

Furthermore, as for memory and complexity analyses, there's lots of work that doesn't overly restrict expressiveness and yet can infer time, space and complexity bounds, among a few I easily found or have seen before:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142....

https://www.microsoft.com/en-us/research/publication/speed-p...

https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/publik...

https://www.cs.ru.nl/~marko/research/pubs/2007/TFP2007.pdf

Not that I think these are perfect solutions, I'm just pointing out that heavily restricting program expression has various approaches, and a brute force expressiveness-limiting hammer isn't the only way. I sympathize with your goal of wanting to reduce expressiveness to make analysis easier, but that makes the project less attractive as well because targeting it is much more work, and it has strictly limited application due to those restrictions.