Unfortunately the author is not very explicit on the interesting formal stuff: 1.implicit and 2.explicit proof-carrying code and 3. verifying compilers with its

Unfortunately the author is not very explicit on the interesting formal stuff: 1.implicit and 2.explicit proof-carrying code and 3. verifying compilers with its cost (there are as of today exactly 2 general usable and fully verified compiler implementations: compcert and cakeml), 4. lowering languages to Isabelle or other interesting proof systems as compiler backends (or using codegen for source code and proof like what cogent does). The author appears also not to know formally proved and domain specific languages, which are "Effect systems" (they check if conditions are uphold) to generate C code. Generally life is a tradeoff and the same holds for showing semantically expressive properties (or one needs a proof system). Most languages rely on LLVM and its linker with linker speak, which are both not formally proven to be consistent and both have no model. The spec also does only describe basic hardware abstraction and without a formal model from CPU vendors this wont improve much. "Cost-model type systems": only sel4. check the blog of the head with papers why https://microkerneldude.org/ https://microkerneldude.org/