I have no idea what Gabriel is intending here; I'm just talking from general knowledge about consistent languages like the CIC. There are a number of general e

I have no idea what Gabriel is intending here; I'm just talking from general knowledge about consistent languages like the CIC. There are a number of general examples, though. 1. You can leave termination guarantees in foreign code up to the programmer using an "unsafe" marker. 2. You can model effects using a monad 3. You can model the whole program as codata which is "driven" by the runtime 4. You can write a compiler of an embedded language in CIC and execute complete programs in, say, C