Sure, you can build a flimsy deathtrap house on top of a solid foundation in a lot of contexts. But if the foundation is unsound, it doesn't matter if your Ada is formally verified or not.

At least the Ada folks acknowledge that the language isn't perfect, and don't pretend they were the very first one on its field.

I don't see anyone pretending any such thing about WebAssembly or WASI. If anything they are drawing on the decades of experience with bytecode formats and security research.

Apparently not, otherwise bounds checking inside of the same linear memory segment would actually be supported.

Likewise, they wouldn't "forget" the formats that already had support for languages like C when talking about what is "new" with WebAssembly.

> bounds checking inside of the same linear memory segment

That can be supported in the source language.

Which is meaningless for module consumers and hardly any different from native processes.

AIUI, wasm does support using multiple linear memory segments at the same time. You don't get that on native processes short of using memory segmentation, which no modern architecture supports.

CPUs like SPARC ADI and ARM MTE offer much better memory protection than what is being sold by WASM.

Solaris, iOS and future Android versions take advantage of their existence.

Which is completely irrelevant as by definition they are not portable.

The fact remain that wasm module have a very well defined behavior when embedded in other applications and can be embedded in a portable way.