When I transferred into the "Oak" group that later became the "Java" organization, the team I was on was looking at whether or not you could write an OS in Java sort of in spite of its safety rules. This sort of concept has been revisited by Rust with its safe/unsafe modal operation.
What both of those efforts have in common is that determining safety may be impossible at the construct level but provable if you were to exhaustively search all possible outcomes.
What the paper and your comment add to the discussion is the intriguing idea that you could create a 'safe' backend (say the equivalent of the JVM) as a target for a C compiler. And code that could not be compiled would be flagged for later analysis. Much like VHDL can express hardware that cannot by synthesized you might end up with a C compiler that could compile code that could not be executed. I could be fun to spend a bit of time poking around that rabbit hole.