It occurs to me that ASM.js (before WebAssembly) was full of jets. That is, they wrote weird idioms that the interpreter could understand and optimize, while technically keeping the semantics of the language itself (JavaScript). The most visible example was someVar|0, which was a kind of way to assert that the expression would be an integer. Not really a type declaration, since it didn't ensure someVar would be a number, only that the expression was integer.
In the examples though, clearly the goal is to have some provability in the core language, make that provability feasible with a small language, and keep that as the language becomes further optimized. It seems subtly different than an optimizing compiler.
Somebody mentioned "failure of full abstraction" on HN a few months ago (actually they said something a bit different), which I tracked down to a late 90s paper by Martin Abadi. It refers to a situation where the object code is exploitable because it doesn't fully reflect the semantics of the source code.
One use of jets, in the secure code setting, is to provide a core language that is so simple that it can obviously be compiled in a "fully abstract" way.
In the examples though, clearly the goal is to have some provability in the core language, make that provability feasible with a small language, and keep that as the language becomes further optimized. It seems subtly different than an optimizing compiler.