This is cool work. Peter Sewell has been giving talks about this, and he is a great speaker. Here is one from this year's EuroLLVM developers' meeting, including some demos of the Cerberus tool: "The Cerberus Memory Object Semantics for ISO and De Facto C" https://www.youtube.com/watch?v=SI3uycKDH8Y
This is scary. I love and hate C, been using it almost 40 years. Its use seems more and more like juggling razor blades, wishing not to get cut but still always wondering when it will happen next.
Rust, Pony, Crystal, Go, Elixir, Haskell, OCaml, Lisp, Clojure have their merits to address most of C's shortcomings, offer much higher levels of abstraction (productivity) and provide these features that didn't yet exist when C grew up. Languages were mostly built bottom-up.
But really, C is often used as a portable-ish lingua franca, along with similar but different: JVM bytecode and LLVM IR, for writing nearer to bare metal (native assembly or runtime).
C hit it big in the 1980s as a language that was portable between smaller (PDP-11) and larger (VAX) minicomputers as well as microcomputers that had a 16-bit address space at best with memory management limited to switching a bank of ROM in and out.
I spent about $80 for a C compiler that run on the OS/9 operating system on my TRS-80 Color Computer. When I upgraded to a PC with MS-DOS there was a Microsoft C compiler that cost about $500, a Turbo C Compiler from Borland that costs around $100 and Tom Mix had a compiler that cost about $20. This was long before GCC.
C was astonishingly portable across machines of variable capabilities; I remember many Unix games like Nethack that would run on MS-DOS as well as they did on Sun workstations. Commercial C compilers supported a multiplicity of "modes" to work with the strange segmented architecture: for instance you could have a 64k address space for data and 64k code.
My favorite language of the late 1980s was Turbo Pascal which had extensions to support systems programming but was a better language than C in most respects and had OO extensions that were much easier to use than C++. I switched to C when I went to college though because I had access to Sun Workstations where C was the way to go.
GNU tools were already establishing themselves as the Cadillac of userspace (e.g. there wasn't commercial competition to make a better awk for HP/UX) but it was another three years before Linux came around and 32-bit x86 chips were starting to whup SPARC and PA-RISC on performance, never mind price-performance.
It was only about 1986 that AT&T was lifted the ban that prevented selling UNIX, which triggered the law suit against BSD a couple if years later.
The damage to other commercial OSes was already done by then.
I got to use Turbo C in 1992, after a couple of years with Turbo Basic and Turbo Pascal. Thankfully the teacher that brought us Turbo C, also had a copy of Turbo C++ 1.0 around.
So Xenix was the only UNIX where I was forced to use C, and a couple of university assignments a few years later.
Everywhere else, just following Bjarne's footsteps, I enjoyed C++ on UNIX, even with the quirks of catching up to C++ ARM.
You're not going to get away from C in osdev anyway, at least not for a long while. It's deeply entrenched in very large operating system codebases (think: Linux and GNU, FreeBSD, OpenBSD, Plan 9 [though they use a slight dialect of C]).
I never found any programming language which i love.
I've settle for rust and go.
What i want is a language which is as simple as Go but we can mark off the portions of program and go one level down to optimize the hell out of it in rust style.
