Vlákno názorů ke zprávičce AdaCore a Ferrous Systems budou vyvíjet Rust pro bezpečnostně kritické aplikace od Pavel Tišnovský - Zajimave. Musim se podivat na to, jak moc...
-
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
