On 30-Apr-21 11:17, heby wrote:
>
> I dlaczego LEON czy RISC-V miały być do tego gorszy niż Heńkowy 8051?

Formalnie nie są gorsze, są inne. Tak więc trzeba na nowo weryfikować
czy realtimowe założenia z Heńkowego 8051 są spełnione w nowej
architekturze.

> Nie przesadzajmy. Tych milionów lini kodu *NIKT* nie zweryfikował
> formalnie. Tam jest weryfikacja przez zasiedzenie. [...]

Tego nie wiemy ani (prawdopodobnie) Ty, ani ja ...
Jednakowoż po coś powymyślali DO-178 i inne wynalazki ...

> 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ł.

A co Ty z tym git-em ciągle ... Jak Heniek ma certyfikowany proces
notowania w kajeciku która z nowych wersji jest najnowsza to ma się tego
trzymać a nie kombinować z git-em ...

> 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.

IMHO zupełnie niesłusznie się spodziewasz. Programiści nie są od
formalnego dowodzenia poprawności algorytmów ...

Piotrek