Would you rather run a formally verified application on top of a conventional kernel/compiler toolchain, or a conventional application on verified kernel/compiler toolchain? Why?
Related Posts
Delighted to see that Typescript 7 is moving to conventional LSP for its IDE services!
https://devblogs.microsoft.com/typescript/progress-on-typescript-7-december-2025/#resetting-language-service-issues
I would have thought that invoking a C compiler would be a solved problem. Looking at Rust's cc crate there's a remarkable long tail of corner cases to fix.
Exotic CPUs, microarchitectures, compiler differences, operating system differences, etc.
https://github.com/rust-lang/cc-rs/blob/main/CHANGELOG.md
Some delightful examples of good compiler error messages in the latest Gleam release: https://gleam.run/news/context-aware-compilation/