Názor k článku
Udržitelné programování s Rustem od Pet - SPARK je super, ale použiteľný pre embedded systémy...

SPARK je super, ale použiteľný pre embedded systémy a podobne. Má dosť silné obmedzenia (teraz hovorím z pohľadu SCADA systémov - do tej "rozumnej podmnožiny" sa bohužiaľ nezmestíme). Pekné je, že sa dá kombinovať SPARK / ADA (niektoré procedúry/funkcie môžu byť SPARKové, s overenou korektnosťou, zvyšok ADA).

SPARK/ADA sa použila aj pri programovaní študentských cube-satov:
https://blog.adacore.com/ten-years-of-using-spark-to-build-cubesat-nano-satellites-with-students

https://www.youtube.com/watch?v=YlnfyToUwv4

Tu:
https://youtu.be/YlnfyToUwv4?t=461
píšu, že majú cca 10 tisíc riadkov kódu. Ok, my máme vyše 2.5 milióna (bez prázdnych riadkov a komentárov).

Tu:
https://youtu.be/YlnfyToUwv4?t=89
hovorí o tom, že z 12 univerzitných CubeSatov sa ozvali po vypustení iba 4, z nich dlhodobe (vyše 2 rokov) fungoval iba ich SPARKový. Ostatné boli programované v C-čku a jeden z nich pošiel v priebehu dňa, druhý do týždňa a tretí vydržal 4 mesiace.