Vlákno názorů ke zprávičce AdaCore a Ferrous Systems budou vyvíjet Rust pro bezpečnostně kritické aplikace od Ink - Trošku off-topic (k tématu coreutils v Rustu) -...
-
Trošku off-topic (k tématu coreutils v Rustu) - clap se ve verzi 3.0.14 zaměřil mimo jiné na velikost binárky a pouhá změna verze z 3.0.10 na 3.0.14 mi ušetřila cca 36 KB v binárce (před i po s LTO a stripem). Snad to takhle půjde dál.
Jinak si myslím, co se tématu týče, že pokud se tahle iniciativa AdaCore a Ferrous Systems povede, může to mít benefit pro oba jazyky a budoucnost oboru jako takového.
-
Iniciativa je to rozhodně parádní a pokud se uchytí, budeme rádi všichi. I z toho důvodu se mi líbí Oraclí projekt GraalVM, mít k dispozici ekosystém, kde si budu moci vybrat jazyk, ve kterém chci danou funkcionalitu naprogramovat, vypadá lákavě.
Nakonec všechny jazyky mají něco do sebe, žádný není lepší nebo horší, takže možnost výběru dle individuality každého z nás jen a jen vítám a už teď se těším, co nám budoucnost přinese. Toho si všimli i někteří autoři materiálů z learn.adacore.com, kteří píší o tom, že dnes již není samotná volba jazyka tak důležitá a zveřejnili materiály pro přechod vývojářů se zkušenostmi z jazyků C++, Java a nově i C, ano, naučit se pokoře je parádní věc.
-
Bylo by fajn, kdyby něco jako GNATprove vzniklo pro LLVM. To by fungovalo bez ohledu na konkrétní jazyk a ve spojení třeba se Z3 by to byl mocný nástroj.
To se bojim, ze by takhle univerzalne by nefungovalo. V deduktivni verifikaci je dulezite, jak se ten ktery jazykovy konstrukt prelozi, aby byla co nejvetsi sance, ze teorem provery prislusne formule automaticky dokazou...
Takze podle me je spis cesta mit specializovany frontend pro kazdy jazyk a pak obecny dokazovaci backend. To je vlastne pripad SPARKu a why3 - GNATprove je frontend pro why3 + dalsi veci okolo (ruzne cachovani vysledku, "preklad" vystupu - hlavne counterxamplu - why3 do SPARK, ...):
