Semantics based compilation
Compilers, as we know them today, will no longer be needed
-- Grigore Rosu
Semantics-based compilation (SBC) is one of the most challenging components of the K framework. Its goal is to automatically generate a correct by construction compiler by applying the semantics of a language to a program written in that language. The result is a new semantics that is a synthesis of the original semantics of the language but specialized for that particular program. The new semantics is simpler, faster to execute and easier to understand.
For IELE, this means that now we can write smart contracts in any programming language and have a correct by construction compiler to IELE.