On 01/10/2019 08:27, AK wrote:
>> Zabawne, bo w kilku krytycznych miejscach i za duże pieniądze się
>> używa. Firmy kupują choelrnie drogi soft robiący to samo, ale od
>> różnych producentów tylko po to aby się upewnić że działanie ich kodu
>> jest zamierzone a nie tylko że to artefakt narzędzia.
> Hehe. Gdy sie wybralo takie nieweryfikowalne barachlo jak C/C++
> do rzeczy krytycznych, to sie trzeba pozniej takimi "technikami
> weryfikacji" podpierac :)

Trzeba się nimi podpierać ponieważ niezwykle mało rzeczy na tym świecie
jest formalnie zweryfikowane a w dodatku nawet jaki jest to bywa że
tylko teoretycznie. Przykładowo można sobie w d... wsadzić jądro L4 z
całą ich weryfikacją jak się okaże że CPU ma buga sprzętowego.