GHC Core is well-typed in contrast with STG which is untyped, but must maintain some properties which are not defined formally. Also some transformation cheats here and there because it "just works". These are the worst C practices. It completely violates the Haskell philosophy.
Conversation
The future low-level IRs must be extremely precise, and it is possible with an advanced type system: dependent + linear types
2
2
8
So Formality?
1
2
or Idris2
1
2
