Underrated language for this space: ATS from the ML family, which has a feeling of what if C met SML/OCaml then graduated.
You get more flexibility for memory safety with linear types over affine types like Rust for preventing double free or use after free-like errors (while be general for any use-X-times problems). Refinement types can enforce bounds. Dependent types + viewtypes can build complex, but zero-cost abstraction for your own code or as wrappers over C libraries to make them safe & pushing checks to the compile phase rather than runtme. On top of that, there are proof-level types/values you can interleave in your code instead of using an auxiliary language like Coq or Agda. Compiling/mapping to C you use a lot of the same tooling of C as well as performance charactistic of C (can opt in/out of GC, unboxed types, can layout the memory, as well as TCO); you also get the stable C ABI over Rust’s general difficult to be used in non-Rust projects.
All this to say you have a language that can operate at the system level, type abstractions that go beyond posterchild Haskell, & a proof language to turn those white papers into proof code right in the project. If it didn’t have a special learning curve, it should be a lot more popular in this space.
Underrated language for this space: ATS from the ML family, which has a feeling of what if C met SML/OCaml then graduated.
You get more flexibility for memory safety with linear types over affine types like Rust for preventing double free or use after free-like errors (while be general for any use-X-times problems). Refinement types can enforce bounds. Dependent types + viewtypes can build complex, but zero-cost abstraction for your own code or as wrappers over C libraries to make them safe & pushing checks to the compile phase rather than runtme. On top of that, there are proof-level types/values you can interleave in your code instead of using an auxiliary language like Coq or Agda. Compiling/mapping to C you use a lot of the same tooling of C as well as performance charactistic of C (can opt in/out of GC, unboxed types, can layout the memory, as well as TCO); you also get the stable C ABI over Rust’s general difficult to be used in non-Rust projects.
All this to say you have a language that can operate at the system level, type abstractions that go beyond posterchild Haskell, & a proof language to turn those white papers into proof code right in the project. If it didn’t have a special learning curve, it should be a lot more popular in this space.