Vlákno názorů k článku
Certifikovaný překladač pro jazyk Rust je tady
od Wavelet - Certifikovaný, bezpečný kompilátor je jedna věc, ale verifikovaný...
-
Certifikovaný, bezpečný kompilátor je jedna věc, ale verifikovaný kód druhá. Nebo se pletu? Můžu mít přeci C kompilované certifikovaným kompilátorem, ale přesto nemusí být korektní. Jako, že certifikovaný kompilátor pořád nenahrazuje verifikovatelný Ada SPARK kód. Rust do teď, pokud se nepletu, nemá specifikaci ani žádný formální důkaz/garanci správnosti (byť na tom někdo dělal myslím). Zkušenější rustafariáni poradí. Dík.
6. 10. 2023, 08:57 editováno autorem komentáře
-
"je to podminka nutna" - ani to podle mě není pravda
Na škodu vidím to, že zde autor zprávičky popustil uzdu své překladatelské iniciativě a slovo kvalifikovaný/qualified (tak jak se používá na phoronixu a webu projektu) nahradil slovem certifikovaný/certified.
Rozdíl vidím v tom, že se certifikuje produkt jako (třebe elektro-mechanický) systém. A to se ještě netvrdí o jeho funkčnosti, ale stanový se jakési "functional safety goal" (třeba při rozsvícených světlech v autě ztráta komunikace (světlometu) neznamená jejich zhasnutí), ke kterým se přiřadí míra závažnosti a stanový se úroveň, se kterou se jim chci vyhnout (ASIL D). Poté musím udělat vše, co po mě požaduje norma (ISO 26262) pro danou úroveň bezpečnosti (ASIL D), abych toto tvrzení prokázal.
Norma po mě nepožaduje, abych použil (ISO 26262, ASIL D) kvalifikovaný překladač, ale pokud ho použiji, tak nemusím prokazovat, že ze zdrojového kódu překladač vygeneruje to co má. To však neříká nic o zdrojovém kódu nebo o hw, na kterém kód běží, ten je potřeba podchytit jinou analýzou.Obdobné normy kromě aut a průmyslové automatizace existují i pro vláčky a letadla. Army a space jsou v tom trochu nepodchycené. To, že je celá problematika funkční bezpečnosti netriviální lze podle mě pochopit třeba sérií článků na dfens . A ani já nejsem funcional safety engineer
-
Todle rozhodne neni pravda - je mozne kvalifikovat rovnou vyslednou binarku a je jedno, jestli ji vytvoril prekladac a nebo naprimo inzenyr v nejakem hexeditoru. Pouziti kvalifikovaneho prekladace muze mit vyhodu v pripade cileni na vice ruznych platforem, castych updatu kodu a tak, ale rozhodne to neni nutnost.
-
Rust to nemá a v současné formě ani mít nemůže. Někdy před rokem jsem viděl nějaký projekt, kde míchali Rust se SPARKem, ale to tam pak nedává moc smysl ten Rust. Že by Rust dostal lepší typový systém taky nehrozí (řekl to sám autor Rustu s tím, že kdo chce lepší typový systém, má použít Lean, kdysi tu byl odkaz na jeho výrok). Takže tak.
