Comment by ArtixFox

Wait just 20% thats a low number damn. You said a lot and i was expecting...idk, 50%?

If Ada was used in domains where rust is used, like desktop applications, servers, high perf stuff, it would also do unsafe stuff you could never verify using spark.

But instead it is used in microcontrollers with runtimes provided by adacore and other vendors. Can you fully know if those pieces of code are 100% verified and safe? the free ones are not. atleast the free x86 one.

How ridiculous. The language you use is not memory safe btw. unchecked_deallocation can be easily used without any pragmas iirc. You need to enable spark_mode which will restrict you to an even smaller subset! You cannot even safely write a doubly linked list in it![you can with great pain in rust] [with less pain in Frama-C] [never tried ats]