The thing is that C is formal by itself. Opcodes, Assembly, C, Python, Common Lisp,… are all equivalent to each other, meanings there’s no statement and no algorithm that you can’t map to each other. That’s what it means to be Turing Complete.

The main issue is that not everyone cares about the semantic of what they’re writing. You don’t need to know assembly to talk about C’s semantic or know C to talk about Python semantics. It does not require going up and down some abstraction tower.