[tel]

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