Get Started with Open Source Formal Verification [video]

fosdem.org

71 points·0rzech··2 comments

Nice to see Fabien here presenting, a nice change to the usual suspects :-) with his down-to-earth embedded personal angle. More people taking time to explain and evangelize amazing tech makes me happy. Go Fabien!

By the way, if you want to know more and dive in, we just completed a 3-days training sessions with AdaCore's Yannick Moy and all the colleagues (some not even Ada practitioners) are itching to put some SPARK everywhere, and were surprised the tech is so accessible, mature, for non-formal-praxis people. We're probably going to book a second session for mostly C dev people.

Give it a try!

(I have no stakes there, but wanting devs to focus on safety, security and better software - more direct value in our daily work)

It's also worth mentioning that Ada and SPARK are very easy to pick up these days. There's Cargo-like tool Alire [1], official VSCode plugin [2] and Open VSX plugin [3], Ada Language Server [4], Emacs Ada mode [5] and GNAT Studio [6]. With Alire one can easily install GNAT FSF builds (meaning GPL with linking exception) and SPARK tools. All libre software.

Not to mention Ada being really versatile and well thought out language. And there's upcoming Ada 2022 standard [7].

[1] https://alire.ada.dev/

[2] https://marketplace.visualstudio.com/items?itemName=AdaCore....

[3] https://open-vsx.org/extension/AdaCore/ada

[4] https://github.com/AdaCore/ada_language_server

[5] https://www.nongnu.org/ada-mode/

[6] https://github.com/AdaCore/gnatstudio

[7] https://learn.adacore.com/courses/whats-new-in-ada-2022/inde...

Reply on news.ycombinator.com