| So there are languages that can do these things individually: Dedalus is an evolution of datalog, incorporating the notion of time in the type system. You're better off working with an abstract version of time, for portability reasons - the compiler can look at the timing specs to optimize resource usage, otherwise you're into VHDL territory and your only recourse is simulation of your system to reason about it, due to complexity . Fine grained energy usage would be specific to say the SOC you're using, eg. for the CC1310 there are specific modes for low power. The compiler could potentially take care of this, but you would probably require an abstract state machine for it to optimize, eg. identify periods to go in to low power mode. Hard realtime nearly precludes many languages due to their need for GC - there are a few realtime GCs around, but really it's better to use a language that has managed memory without GC.
So after all that, you're down to a handful of suitable languages for realtime eg. Rust or Composita. Lastly, guaranteeing program correctness is something you need to do in a high level language, to be able to capture the semantics you're tying to prove. ie. you need a language that can express higher order logic. Whether this proof step is intrinsic to the language is up to you, but you then need to map the higher-level model to your low level language. Several projects do this eg. CakeML, but the full self-verified OS doesn't exist as yet. Interestingly there is a linguistic solution for all of this which I'm working on, just not got anything concrete to share yet - maybe in 6 months :) |