On 30/04/2021 11:01, Piotrek wrote:
>> Mamy całkiem sensowne procesory współczesne do cieżkich zadań, których
>> programowanie jest "normalne" i nie ma problemu ze znalezieniem
>> programistów.
> Ale rozumiesz, że może też chodzić o formalne dowodzenie poprawności
> algorytmów.

I dlaczego LEON czy RISC-V miały być do tego gorszy niż Heńkowy 8051?

> I przeniesienie kilku milionów linii kodu z 2 czy tam 9 słabszych ale
> zestandaryzowanych komputerów na jeden super-duper ale bliżej nikomu nie
> znany może oznaczać grube miesiące jeśli nie lata i dziesiątki albo
> setki milionów w brzęczącej monecie, które trzeba poświęcić na retesty,
> certyfikacje, etc.

Nie przesadzajmy. Tych milionów lini kodu *NIKT* nie zweryfikował
formalnie. Tam jest weryfikacja przez zasiedzenie. Jesteśmy w czarnej
d... jeśli chodzi o weryfikację dużych systemów, niby rozwijamy się,
tworzymy nowe metodyki, ale powiedz to Heńkowi, co gita na oczy nie widział.

> I z całym szacunkiem, ale programiści Ci tego nie zrobią bo się po
> prostu na tym nie znają.

Zależy jacy programiści. Po tych w lotnictwie, spodziewam się że
potrafią formalnie dowodzić przynajmniej kilkuset linijkowców dbających
o bezpieczeństwo. Których pewnie nie ma, za to są wciśnięte właśnie
kilkumilionowe potworki do sterowania autopilotem i sterowaniem klimą w
jednym.