If you're in the business of developing ultra-low-defect software, and you aren't committed to C, SPARK Ada is another option.
[0] https://learn.adacore.com/courses/SPARK_for_the_MISRA_C_Deve...
I imagine the compiler situation would need to change before this could become a possibility. I doubt off-the-shelf Rust/LLVM is appropriate for compiling life-and-death code.
I imagine it would also be necessary to strictly control memory management, using pools rather than doing the equivalent of malloc/free. It seems Rust has a crate for that: https://docs.rs/heapless/0.5.5/heapless/
> I've only ever met one engineer who actually liked coding in Ada.
It certainly lacks many luxuries. For that matter, it also lacks basic examples. I tried to dabble with Ada recently, and pretty quickly ran into trouble (I was unable to figure out how to instantiate any of GNAT's 'bounded containers').
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Containers.Bounded_Vectors;
procedure Main is
package BV_Integer is new
Ada.Containers.Bounded_Vectors (Index_Type => Positive,
Element_Type => Integer);
use BV_Integer;
Vec_Max : constant := 10;
Vec : Vector (Vec_Max);
begin
Put_Line ("Appending some numbers...");
for I in 1 .. Vec_Max loop
Vec.Append (Integer (I));
end loop;
Put_Line ("Appending another number...");
Vec.Append (Vec_Max + 1); -- this raises an exception.
end Main;