Дмитрий Волков. HIGH-ASSURANCE EMBEDDED

Сейчас почти каждый носит в своём кармане более 40 млн строк кода только на C, ездит в машине, управляемой бортовым *компьютером*, живёт в доме, подача воды к которому регулируется SCADA или на удалении менее 400 км от АЭС.
Я расскажу, что может пойти и идёт не так, как с этим жить и какие технологии разработки ПО используются для того, чтобы делать самолёты, которые (из-за сбоя электроники) не падают, машины, которые останавливаются при нажатии на педаль тормоза и ракеты, которые взлетают: в частности, речь пойдёт о memory-safe языках в embedded (Rust) и program extraction из Haskell (Ivory) и Coq + runtime verification à la Agda.

Видео Дмитрий Волков. HIGH-ASSURANCE EMBEDDED канала Fp Conf