Názory k článku
AdaCore a Ferrous Systems budou vyvíjet Rust pro bezpečnostně kritické aplikace
-
Pavel TišnovskýZlatý podporovatelZajimave. 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/variants) 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#
-
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 -
Ked sa dostanes do fazy, ze ti budu predhadzovat projekty typu "ono, to funguje, len to treba trochu opravit" pretoze budu vediet ze to das, tak budes mat na vec uplne iny pohlad. Ako, pre mna zamna nech si kazdy programuje ako chce a v com chce, mne pride zbytocne ked treba nieco po niekom opravovat a prerabat (tym nemyslim chyby v kode ale v celkovej koncepcii aplikacie). Mozno u teba sa to prejavi tym, ze budes neurotik s chutou lamat ludom ruky, ale to je evidentne este vo hviezdach.
-
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
-
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
-
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.
-
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ů.
-
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.
-
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í.
Nemyslim, ze by timhle AdaCore planovala zariznout Adu. Hlavne v leteckem, zeleznicnim a vojenskem prumyslu je porad dost i novych Ada projektu a AdaCore by byla proti sobe, kdyz by chtela tenhle trh opustit nebo i jen vysilat signal, ze s Adou nepocita. Takze v tomhle smyslu myslim, ze Ada ma celkem dlouhou budoucnost.
Horsi to je uz s potencialem růstu (na tohle slovo jsem si zapnul diakritiku ;) Ady a schopnosti tlacit ji novym zakaznikum. Tady myslim, ze AdaCore pochopila, ze snit o tom, ze Ada bude zas mainstreamovy jazyk a pocitat s tim, ze bude nejak vyznamneji rust neni dobra strategie.
A naopak SPARK ma podle me celkem jasny potencial. Ale nikdy to nebude mainstreamovy jazyk - potrebuje mit vedle sebe vetsi jazyk tak, aby mohli lidi snadno psat kritickou cast systemu ve SPARKu a dalsi casti v necem jinem. A tady AdaCore asi pochopila, ze presvedcovat potencialni zakazniky (kteri treba z velke casti pouzivaji nebo premysli o Rustu) at zkusi SPARK a jeste k tomu prejdou na Adu neni to prave orechove. Lepsi strategie bude prodat jim podporu Rustu a pak se s nimi bavit o SPARKu (integrovanem s Rustem). A pak se s nima pripadne budou moct bavit i o te Ade...
Mimo jine AdaCore prodava i podporu pro C/C++:
https://www.adacore.com/c-toolchainsCoz je zase pragmaticke rozhodnuti - AdaCore pracuje na GCC a takhle muze zpenezit svoje know-how. Vetsina jejich Ada zakazniku bude v nejake forme pouzivat i C/C++, tem muzou prodat podporu C/C++ bez vetsi marketingove snahy a soucasne muzou pritahnout i nejake ne-Ada zakazniky se kterymi se pak muzou pripadne bavit i o SPARKu a Ade.
-
Výborně napsáno, ano, vypadá to, že Ada z letectví, námořního průmyslu nebo vlakové a automobilové dopravy jen tak nezmizí, jen ty projekty nejsou zvenku vidět, což je pochopitelné, ale v dnešním stále více otevřeném světě poněkud nedůvěryhodné.
AdaCore je komerční firma, která musí vydělávat, proto její model chápu - i GNAT Studio uvádí oficiální podporu pro C a C++, souhlasím, že se jedná o pragmatické rozhodnutí a osobně bych v dnešní době nejednal jinak.
Pokud vývojáři z této společnosti přispívají do gcc-ada, tím lépe, mimochodem moc se těším na další verzi GNAT Studia, už je opravdu nejvyšší čas zbavit se Pythonu 2 a přejít na aktuální verzi.
Hmm, takže stmelení Ady a Sparku s Rustem je možná jediné rozumné řešení, to sedí. Je to začarovaný kruh, nový projekt v Adě je problematický pro naprostý nedostatek vývojářů, kteří zase nemají motivaci jazyk se učit (mimo jiné kvůli některým mýtům, které postupem času naštěstí mizí, má-li člověk motivaci si je ověřit).
O to raději se do studia Ady/Sparku a nakonec Rustu pustím, musím si přečíst nebo vyslechnout pár názorů a zkušeností, abych motivaci opravdu měl (a nemusel se do nekonečna vracet k Pythonu, který uznávám stejně jako všechny ostatní jazyky, ale nijak zvlášť mi nesedí, to holt máme každý jinak).
-
"O to raději se do studia Ady/Sparku a nakonec Rustu pustím, musím si přečíst nebo vyslechnout pár názorů a zkušeností, abych motivaci opravdu měl (a nemusel se do nekonečna vracet k Pythonu, který uznávám stejně jako všechny ostatní jazyky, ale nijak zvlášť mi nesedí, to holt máme každý jinak)."
No mně taky Python nikdy moc nevyhovoval, ale to je subjektivní. Adu rozhodně doporučuju a Rust taky (možná i v opačném pořadí), SPARK bych si nechal až nakonec a i tak si nejsem jistý, že ho člověk uplatní, je to dost specifická záležitost. Nicméně určitě je dobré vědět, jak funguje a proč se používá v bezpečnostně kritických aplikacích. Držím palce při učení ;)
-
Přesně tak, volba jazyka je subjektivní a člověk se holt musí rozhodnout. U mě to docela dlouho trvalo (stejně jako např. výběr linuxové distribuce), ale nakonec jsem zjistil, že jako obyčejný člověk mám nejraději jazyk, který se mě jak tu jeden z diskutérů trefně poznačil snaží vést za ruku a osobně jej vnímám jako nejčitelnější z dostupných možností. Ano, se zkušenostmi s Pythonem jsem také nejdříve uvažoval o Rustu, Cčková a Pythoní syntaxe je pro mě však dosti kryptická a když se podívám na program psaný v Adě, hnedle je mi jasné, oč kráčí (i když uznávám, že jednoduchý program, který mi na jednom řádku vypíše, kolik má moje počítadlo procesorů, se skládá se dvou souborů a bez komentářů mají oba 21 řádků přesně jak to voko v kartách).
Holt oba jsme asi dost ukecaní, tak si sedneme. I takové na první pohled hlouposti, jako cykly, které mi v Adě připadají jasné a u jiných jazyků bádám, pro mě poněkud nešťastná céčková "++" inkrementace nebo operátor přiřazení, který je v Adě jasně vymezen vedle porovnání mi dost pomáhají v orientaci v kódu. Plus nezanedbatelná je opravdová zpětná kompatibilita, kterou jsem uváděl výše a sám testoval, četl jsem, že programy pro vojenství musejí fungovat tak jak jsou minimálně 30 let (fíha), takže pokud jazyk i toto splňuje, je to jen další plus. Přitom jako uživatel Archu mám rád novinky, Ada se ale přes svůj poněkud dinosauří původ stále vyvíjí a nástoje okolo také, už aby vyšla ta 202x.
Takže za mě rozhodnuto, jdu do Ady, poté dle situace uvidím ten Spark a následně Rust. Jak poznamenal můj známý dnes již letitý programátor, člověk bude na vývojařinu nahlížet perspektivou prvního jazyka, ve kterém začal opravdové programy vyvíjet a tak nějak cítím, že u mě by to měla být Ada. Nevypadá to, že by v dohledné době zanikla a pokud ano, je to holt osud, který se má stát, život jede v pohodě dál.
Třeba nás AdaCore s Ferrousákama nakonec překvapí a vytvoří i operační systém využívající tyto dva jazyky, uvidíme. Rozhodně bych byl pro, aby vedle dokumentů Ada pro C/C++/Java vývojáře vyšel i Ada pro programátory v Rustu, to vzhledem k aktuální situaci navrhnu v diskuzi.
Děkuji za všechny názory, konečně jsem se rozhodnul. Nakonec příklady z parádních Pythoních kurzů (Pyladies, učebnice pana Pecinovského, Udemy) i šikovné utility z Rustu mohu zkoušet vyvíjet i v Adě, ta holka copatá mi říkala, že zmákne oboje.
-
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).
-
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.
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, ...):
