AdaCore a Ferrous Systems budou vyvíjet Rust pro bezpečnostně kritické aplikace

Díky moc! Zajímavé téma, jako vždy.
Pro mě docela překvapující spolupráce.

3. 2. 2022, 09:08 editováno autorem komentáře

Zdravím, ano, toto je skutečně zajímavé, Rust byl s Adou srovnáván hned v době svého vzniku a byl považován za konkurenta při psaní “bezpečného kódu”. Teď zdá se dojde k symbióze a SPARK bude společným jmenovatelem.

Zajimave. Musim se podivat na to, jak moc bude SPARK omezujici pro realne programy. Protoze pokud ma zarucit vsechny naznacene veci v compile time, tak to asi bude muset mit brutalne dobry/komplikovany typovy system.

Myslím, že typový systém SPARKu se moc neliší od Ady (nejspíš vůbec, od verze 2014 je prý vlastní podmnožinou Ady 2012). SPARK má obecná omezení na kód a pro formální verifikaci se píšou "hinty" (assert, assume, loop invariants/va­riants) pro "dokazovač" (prover), kterých je několik na výběr (nejlepší byl svého času Z3, ale teď už ho dohánějí i některé ostatní). Jde tedy o trochu jiný přístup než třeba u Agdy, kde veškeré ověření korektnosti v době překladu obstará typový systém. Hodně dobrá je tato kniha: https://www.cambridge.org/core/books/building-high-integrity-applications-with-spark/F213D9867D2E271F5FF3EDA765D48E95#

Dik za info + linky!

Není zač. Ještě doplněk (je tam PDF zdarma): https://learn.adacore.com/courses/intro-to-spark/index.html

Jak uz psal Calculon, typovy system je stejny jako u Ady a compile time overovani se dela pomoci data flow analyzy a hlavne deduktivni verifikace (takze nutnost specifikovat pre- a post- conditions funkci a vetsinou i loop invariantu).

Zajimava stycna plocha SPARKu a Rustu je borrow checker. Viz:

https://blog.adacore.com/using-pointers-in-spark
https://books.google.fr/books?id=ZfYPEAAAQBAJ&pg=PA55&lpg=PA55&dq=Veri?cation+of+Programs+with+Pointers+in+SPARK&source=bl&ots=CEkp85pJoG&sig=ACfU3U2T8pi4lK4N9pgtgVGbl7xhYF3f4A&hl=cs&sa=X&ved=2ahUKEwi4z4a_ueP1AhVQBmMBHe_aDBkQ6AF6BAgaEAM#v=onepage&q=Veri%3Fcation%20of%20Programs%20with%20Pointers%20in%20SPARK&f=false

Tak on spark az take obmedzenia pre realny program nepredstavuje. Predstavuje neprekonatelny problem pre velku vacsinu sucastnych programatorov.

Aha. A ty programy má teda psát kdo?

Na to někdo napíše robota ;)

Mně ten dokonalý programovací jazyk bez programátorů přišel jak hospoda na mýtince - jediná její vada je, že tam nechodí lidi. A Ty jsi tam teď dosadil i Ludvíka, který to nakonec celé vyřeší.

Tak sa poupravim, problem s tym budu mat firmy ktore miesto lacnej lopaty budu musiet zaplatit progranatorov preferujucich kvalitny kod, miesto toho aby isli cestov je to lacne a nejako to funguje.

3. 2. 2022, 15:11 editováno autorem komentáře

Moc jsi to nevylepšil. Že se považuješ za elitu, to jsme pochopili už v prvním příspěvku.

Ty asi programátor modré krve. Já budu tebe následovat (vtip).
Naopak jazyky jako SPARK a Ada by mohli spoustě programátorům pomoci. Tyhle jazyky nejsou přechytralé, ale naopak se snaží tě vést za ruku. Díky tomu jsou ale také pěkně ukecané (což mě osobně nevadí).

3. 2. 2022, 14:41 editováno autorem komentáře

SPARK už je asi hodně specifický, má omezení na kód a bez té formální verifikace nemá smysl ho používat, ale Adu (a Rust) je rozhodně užitečné znát. A určitě by si oba jazyky zasloužily větší zastoupení ve výuce na univerzitách.

Tak snahy mozno boli, len zabudli studentom vysvetlit ze to nie je divny pascal a begin sa netreba bat...

Hlavne by odfiltrovali kopu odpadu, cim by dali priestor perspektivnejsim ludom. To by bola hlavne ulava pre dalsich programatorov, ktory by nemuseli robit pestunky. Urob to takto, toto nesmies, odpovedat dokola na preco ohladne tej istej veci a stale dookola...

3. 2. 2022, 16:28 editováno autorem komentáře

Jojo, roste nám celá nová generace Python programátorů :) Samá konvence, kterou musíš někomu neustále vysvětlovat a často ho ani nepřesvědčíš. Já jsem vždy tvrdil, že Python není pro začátečníky :D

3. 2. 2022, 18:54 editováno autorem komentáře

Tak asi protoze si ve skole projdou takovym tim divnym koleckem Python+Java nebo C+Java, takze z tohoto pohledu maji dost maly rozhled. To je ovsem spis chyba tech skol.

Njn, miesto toho aby sa ucili programovat tak sa ucia pouzivat konkretny jazyk.

Moc děkuji za zprávu i zde na rootu, ano, včera jsem na blogu Adacore tuto informaci četl a musím se přiznat, že mě dost překvapila.

O Adu jako jazyk s velmi zajímavými vlastnostmi se zajímám a v posledních dnech se jí intenzivně učím (mám jen základní zkušenosti s Pythonem, takže jsem si pořídil knížku Beginning Ada programming from novice to professional + sleduji web learn.adacore.com, materiály se několikrát ročně aktualizují a v poslední době nabízejí i pdf a epub ke stažení), jen si nejsem jist jak je to s jejím dnešním využitím.

Pokud vím, Ada se na českých školách již neučí, oslovil jsem konzultanta GNAT Academic Program, kde mi však bylo řečeno, že je k dispozici pouze univerzitám a pro vlastní učení musím využít volně dostupné materiály, knihy nebo videa z Youtube např. od Quentina Ochema. AdaCore na svých stránkách uvádí více úspěšných projektů pro železnice, letectví, vojenství nebo automobilový průmysl, evropské konference běží, některé odkazy jsou však dnes již nefunkční a např. zajímavý Ada User Journal není poslední rok vůbec k dispozici.

Ale proč toto píši - mohu se zeptat zkušenějších vývojářů v tomto jazyce, zda je dnes stále perspektivní? Ada má pro mě ze všech jazyků asi nejpříjemnější a nejčitelnější syntaxi, u ostatních je pro mě více či méně kryptická. Stejně jako např. FreePascal (projekt Ultibo) nebo Rust (RedoxOS) v ní lze programovat nízkoúrovňové věci včetně operačních systémů (a toto by mě zajímalo), jen se zatím nikomu nepodařilo něco podobného dotáhnout do konce. Github nabízí nečekanou spoustu projektů (včetně takových věcí jako Matreska - rámec pro tvorbu informačních systémů). Prozkoumal jsem i články zde na Rootu, ty jsou však už poněkud letité a rád bych měl více informací z dneška.

Nezdá se Vám při čtení mezi řádky snaha AdaCore míněná spíše jako postupný přechod na jazyk Rust (což by bylo pochopitelné, přeci jen je modernější a vypadá to, že se opravdu uchytí)? Je to firma, která musí vydělávat a pokud je Ada / Spark projektů málo (a nové již možná nevznikají, na toto mi zatím nikdo nebyl schopen odpovědět), snahu samozřejmě chápu.

Používá některý z čtenářů Rootu Adu aktivně, případně i ve firemním prostředí?

Předem děkuji za odpovědi a omlouvám se za delší příspěvek.

“Nezdá se Vám při čtení mezi řádky snaha AdaCore míněná spíše jako postupný přechod na jazyk Rust”

Tohle v tom nevidím, ale trochu si konkurovat můžou. Ada je v tomto prověřená a hodně firem v ní má spoustu kódu. Než bude Rust nějakým způsobem úředně certifikovaný, bude dost v nevýhodě. Ale budoucnost neumíme číst nikdo, může se stát něco málo pravděpodobného.

Než bude Rust nějakým způsobem úředně certifikovaný, bude dost v nevýhodě.

To je samozrejme pravda, ale tohle je dost specificke pouziti.

Mě to přijde jako geniální marketingový tah. Kdo bude potřebovat může verifikovat jen části kódu ve SPARK, "značka" Ada neupadne v zapomnění a pro celý projekt lze používat nedosažitelný komfort Rust ekosystému. Ada je na tom dnes s ekosystémem bídně. Žádný package manager (kecám: https://blog.adacore.com/first-beta-release-of-alire-the-package-manager-for-ada-spark :D), ne moc knihoven. Když se na to podíváš tak zjistíš, že prakticky ji dnes je schopen nasadit jen AdaCore, takže monopol, a licence GNATu (myslím) taky není úplně bez problémů.

Njn, aj ruby ma skvely package manager, to bude asi dovod preco vacsina softu v ruby nefunguje so systemovymi kniznicami.

Ano, proto mě napadl ten možný přechod na Rust mezi řádky, je to ale jen domněnka, takže počkáme na čas budoucí. Ten Alire už nějaký pátek sleduji, holt pypina, conan nebo cargo ukázali, že tohle je zajímavá cesta a Ada nesmí být pozadu.

Licence GNATu se probírala hodně, pokud rozumím, GNAT GPS a nástoje okolo (ada web server, aunit, gtkada, language server etc.) jsou dnes otevřené a buď si mohu koupit podporu nebo využít zatím uzavřené nástroje (GNAT Pro, QGen apod.), což bych např. jako výrobce lokomotiv nebo letadel určitě udělal (viz moje minulé zkušenosti z firemní sféry, kdy při nasazení SAP R/3 a Oracle bylo poněkud úsměvné uvažovat nad Centosem místo placeného RHELu).

Takže snad ten monopol nebude takový jak uvádíš, na druhou stranu mít za částečně otevřeným řešením komerční firmu není na škodu (viz. např. Oracle, ať už si o něm myslíme cokoliv).

Suma sumárum znalost Ady se neztratí (a na Githubu je opravdu spousta otevřených projektů plus se vesele vyvíjí nástroje pro vývoj - např. modul pro VSCode) a zkombinovat jí s Rustem určitě nebude špatná volba, takže se na ní vrhnu a uvidím, už se těším.

A hlavně tím docela vyšachovali C++. Dle mého to Rustu pomůže víc než Adě.

Když se na to podíváš tak zjistíš, že prakticky ji dnes je schopen nasadit jen AdaCore, takže monopol

Kompilator Ady je normalne soucasti GCC. Na druhou stranu je pravda, ze do Ada frontendu asi moc lidi mimo AdaCore neprispiva. AdaCore naopak prispiva i do jinych casti GCC.

Dal ma AdaCore i frontend pro LLVM. Myslim, ze tady hlavni cil neni opustit GCC, ale byt napojeny i na ekosystem okolo LLVM (nastroje pro fuzz testing, symbolickou exekuci, ...) a pripadne i mit v budoucnu moznost pouzit LLVM backend pokud zrovna bude podporovat nejakou platformu, kterou GCC backend nepodporuje.

Dal jsou i dalsi firmy co porad vyviji Ada kompilator, napr. Green Hills. Ale jo, nevim, nakolik jsou tyhle firmy polomrtve.

a licence GNATu (myslím) taky není úplně bez problémů.
Jo, myslim, ze v minulosti byly snahy AdaCore o triky smerek k tomu, ze programy zkompilovane primo GCC musi mit GNU licenci, ale nastesti prisli na to, ze tudy cesta nevede.

Děkuji za názor, ano, do budoucnosti opravdu nikdo nevidí. Naprosto souhlasím, Ada je prověřená a bezvadně certifikovaná (nové verze nevycházejí tak často, což je však vzhledem k zaměření pochopitelné, na druhou stranu je velmi příjemné, že program vytvořený ve verzi jazyka 83 bez problémů zkompiluji i v aktuální 2012).

Rustu bude zřejmě chvíli trvat, než (pokud) jej firmy opravdu přijmou ve velikém, každopádně integraci Ady a Rustu se nebráním, budou-li dobře spolupracovat, tím lépe pro nás všechny.

Mimochodem nedávno jsem četl zajímavé aktuální shrnutí dnešní Ady zde:

https://neonkaraoke.ru/en/internet/yazyk-programmirovaniya-ada-ada-yazyk-programmirovaniya/

takže s přihlédnutím k tomu, že programování mě neživí (alespoň zatím) a zaměření a především syntaxe Ady mě láká ze všech jazyků asi nejvíce (Python má určitě své kouzlo, jen si jsem stále méně jistý, že se hodí pro začátečníky, jeho volnost nemusí být vždy přínosem a např. veliký informační systém bez využití anotací si neumím v rozumné míře představit), budu v jejím studiu pokračovat, nakonec Ada, Spark a Rust nebude vůbec špatná volba (snad letos vyjde ta slibovaná Ada 202x, aktuální GNAT Studio už její předběžnou specifikaci podporuje).

Dost by mě zajímalo, jestli se tyto okrajové jazyky v dohledné době zmátoží, například Fortran trochu chytá druhý dech (víceméně jako DSL, ale i to je pozoruhodné), dokonce i Prolog si sem tam vrzne (třeba překladač Rustu v sobě obsahuje interpret Prologu).

v ní lze programovat nízkoúrovňové věci včetně operačních systémů (a toto by mě zajímalo)

Viz napr. Muen separation kernel napsany ve SPARKu:
https://muen.codelabs.ch/

Jinak na nizkourovnovnove programovani je zamerena soutez Make with Ada, co vim, tak se tam dali najit i celkem zajimave projekty:

https://www.hackster.io/contests/adacore3

Ale proč toto píši - mohu se zeptat zkušenějších vývojářů v tomto jazyce, zda je dnes stále perspektivní?

To je otazka. Ada sama o sobe ma urcite zajimave featury, ktere v jinych mainstreamovych jazycich nejsou (napr. range types), ale je otazka, jestli to napriklad proti tomu Rustu porad staci. Vyhoda Rustu je nesrovnatelne vetsi komunita, z toho plyne vetsi mnozstvi knihoven, ...

Na druhou stranu SPARK v oblasti deduktivni verifikace nema obdoby (jeho pouzitelnost je zcela jinde ve srovnani s napr. proti Eiffelem, Dafny, Frama C, VCC). Protoze je mozne Adu a SPARK snadno kombinovat (dokonce i v ramci jednoho modulu muzete mit cast funkci v Ade a cast ve SPARKu), tak myslim, ze Ada ma budoucnost spis ve spojeni se SPARKem.

Z posledni doby zajimave nasazeni SPARKu v NVIDIA:
https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/

Děkuji za zprávu, až získám v jazyce více zkušeností, na Make with Ada se určitě juknu, tohle může být bezva výzva např. pro študáky (což už dávno nejsem, he, he, možná naštěstí).

Ano, přesně tak, i proto jsem vydal cestou Pythonu, protože obrovská komunita a veliké množství materiálů je samozřejmě důležité. Jen se mi v něm neprogramuje právě nejlépe, když se juknu na kód v Adě, je pro mě mnohem čitelnější a stále se k ní vracím.

Hmm, ten Spark vypadá opravdu parádně, děkuji za hezký popis. Takže rozhodnuto, pečlivě si projdu knížku Beginning Ada Programming včetně příkladů a budu zkoušet, co se jen dá, poté se juknu na eknihu Learning Ada ze stránek AdaCore (včetně Ady i Sparku) a vytvořím nějaký projekt, který mě zajímá (klidně ncurses aplikaci ála rustí Kmon, evidenci výnosů a nákladů nebo program pro vedení administrativy mých dětských táborů třeba s využitím GtkAda nebo klidně QT6Ada, který jeden šikovný ruský autor drží při životě). Následně nebude od věci i Rust, do té doby bude jasnější jak to s ním AdaCore myslí.

Ještě jednou děkuji za všechny postřehy, názor od někoho, kdo je skutečně v obraze, si velmi cením.

“Na druhou stranu SPARK v oblasti deduktivni verifikace nema obdoby”

Jazyky jako Agda také mají mocné nástroje pro “dedukci” (ve formální logice) v době překladu. Mně je tento přístup (verifikace silným typovým systémem s kvantifikátory) dokonce bližší, studium fyziky mi dalo celkem obstojné znalosti matematiky včetně teorie důkazů a i takových pakáren jako teorie kategorií, takže tento přístup je mi sympatičtější než verifikace ve stylu SPARKu (ale o to více mě SPARK zajímá). Haskell je vlastně srandovní hračka pro prváky, kdo chce skutečně abstraktní (a silný) typový systém, sáhne po Agdě :) Nicméně ta myšlenka sdílených knihoven napsaných ve SPARKu je velice lákavá, přece jen většina vývojářů dá nejspíš přednost imperativnímu paradigmatu.

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.

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, ...):

http://why3.lri.fr/#documentation