you said you use Ada, if you use it, you should know that Ada is fundamentally unsafe language with a safe subset called spark. It could not verify dynamic all

you said you use Ada, if you use it, you should know that Ada is fundamentally unsafe language with a safe subset called spark. It could not verify dynamic allocations thats why it has such a huge toolset for working with static allocations. Frama-C allows you to program in a safe subset of the unsafe language called C. And these languages are the backbone of everything where lives are at risk. YOu can have a language that allows both unsafe and safe. Safety is not binary and our trains run C/C++ [BOTH UNSAFE LANGUAGES]