The competition has three prizes of $2,000 each!

Just came across a donation site for the Alire project.

> Contributing to the Ada open source ecosystem through the Alire package manager for Ada/SPARK

Online participation in the Ada Developers Workshop will be free of charge! It is still a requirement to register. As a reminder, the Workshop's programe has been available for a while, so go ahead an take a look! 🤩

GNAT FSF 14 is now available in a special index branch. Use this command to add the index branch:

alr index "--add=git+https://github.com/alire-project/alire-index#gnat-fsf-14.1" --name=gnat_fsf_14 --before=community And then alr index --del=gnat_fsf_14 to remove it once your done playing with it.

If you have some time to give it a try and give me some feedback that would be great 👍️

#gcc #alire

The list of presentations looks great!

• New implementation-defined aspects and pragmas:
  • Local_Restrictions, which specifies that a particular subprogram does not violate one or more local restrictions, nor can it call a subprogram that is not subject to the same requirements.
  • User_Aspect_Definition and User_Aspect, which provide a mechanism for avoiding textual duplication if some set of aspect specifications is needed in multiple places.
• New implementation-defined aspects and pragmas for verification of the SPARK 2014 subset of Ada:
  • Always_Terminates, which provides a condition for a subprogram to necessarily complete (either return normally or raise an exception).
  • Ghost_Predicate, which introduces a subtype predicate that can reference Ghost entities.
  • Exceptional_Cases, which lists exceptions that might be propagated by the subprogram with side effects in the context of its precondition and associates them with a specific postcondition.
  • Side_Effects, which indicates that a function should be handled like a procedure with respect to parameter modes, Global contract, exceptional contract and termination: it may have output parameters, write global variables, raise exceptions and not terminate.
• The new attributes and contracts have been applied to the relevant parts of the Ada runtime library, which has been subsequently proven to be correct with SPARK 2014.
• Support for the LoongArch architecture.
• Support for vxWorks 7 Cert RTP has been removed.
• Additional hardening improvements. For more information reltated to hardening options, refer to the GCC Instrumentation Options and the GNAT Reference Manual, Security and Hardening Features.
• Improve style checking for redundant parentheses with -gnatyz
• New switch -gnateH to force reverse Bit_Order threshold to 64.
• Experimental features:
  • Storage Model: this feature proposes to redesign the concepts of Storage Pools into a more efficient model allowing higher performances and easier integration with low footprint embedded run-times.
  • String Interpolation: allows for easier string formatting. Further clean up and improvements to the GNAT code.

#nvidia #gpu #cuda #ada

This site provides a simple way to install Ada's toolchain Alire using GetAda.

Did you know that Debian has Aiire packages?!

Fabien is starting a crowdfunding campaign for a pocket groovebox he has been developing on his spare time. Of course the firmware is in Ada 🤩 The sources are on GitHub if you want to have a look.

If you can subscribe on CrowdSupply and send this link to anyone that could be interested, that would help a lot.

A new Muen version with a long change log! 🤩

🔥 Hot news!

Thanks to AdaCore sponsoring the Ada Developer Workshop in Barcelona, the early registration fee for in-person participation will be only 10 EUR, including 🥪 lunch and ☕ coffee breaks.

That’s as low-cost as attending an Ada Developer Room at FOSDEM in Brussels, as you easily spend 10 EUR on food and drinks there… 😉

Registration info, for the conference, tutorials, workshops, social events, will shortly be added to the conference website at Ada-Europe 2024 1.

Hope to see many of you there! And remember, submissions are still welcome!

The March 2024 Meetup just finished! Thanks to everybody who participated.

Quite a few topics were discussed, here is a list of topics and references to them:

• WolfSSL and its Ada binding
• FOSDEM
• Ada Developer Workshop taking place in Barcelona the 14th of June.
  • The (current) submission deadline for presentations is the 31st of March!
  • Online participation is expected. We will try and have a setup to let people participate online!
  • It was created in order to let the wider Ada community have a home to meet and talk about Ada. This is a "response" to the lack of an Ada DevRoom @ FOSDEM the past couple of years.
• Alire v2.0 is around the corner
  • Help test the new Release Candidate 1
  • Mac M1 (ARM64) support is in the works. Thanks Simon and Maxim!
• There is now a list of projects to work on in the main Ada-Lang webpage.
  • It focuses of projects that would help the wider Ada community.
• Ada support for org-mode code blocks (babel) is now going to be part of the official org-mode distribution of Emacs!
  • Thanks Francesc for the work!
• The NSA published a list of memory safe languages
  • Ada was not mentioned in the list of programming languages. Nonetheless Ada/SPARK are listed in the references.
  • Ada needs better visibility and "marketing".
• The GCC 14's Ada changelog section is on its way, stay tuned!

LatenceTech leverages Ada's capabilities to develop innovative network tools. They successfully implemented patented LIFBE process, reducing data volume for bandwidth testing by 90%.

Ada's low-level memory management and concurrency features were crucial for this project. GNAT Pro's real-time capabilities also ensured timely delivery.

This collaboration highlights Ada's suitability for energy-efficient network software and complex real-time systems.

Join the Ada community and empower the next generation of reliable, high-performance software!

TOC:

• J. P. Rosen. “Report on the ASIS BoF Session: The Future of ASIS and Vendor Independent Tools” 221
• C. Dross. “Containers for Specification in SPARK” 249
• S. Tucker Taft. “Rigorous Pattern Matching as a Language Feature” 255
• L. Humphrey. “Basic Formal Verification of a Waypoint Manager for Unmanned Air Vehicles in SPARK”

🎉 NetBSD has got GNAT 13, gprbuild and Alire!

LibMLKEM: a brand new, formally verified implementation of the post-quantum key exchange algorithm ML-KEM, built with the Ada & SPARK.

Why LibMLKEM?

• Rock-solid security: SPARK's formal verification guarantees no errors, leaks, or type issues.
• Independent & transparent: a completely new take on ML-KEM, free from existing code biases.
• Pushing the boundaries: a benchmark for formal verification tools like SPARK, CBMC, and Kani.

Not production-ready yet!

LibMLKEM is for research and demonstration purposes only. It prioritizes security and verifiability over optimization. The constant time property hasn't verified yet.

📆 I would like to announce the March (2024) Ada Monthly Meetup which will be taking place on the 9th of March at 14:00 UTC time (15:00 CET). As always the meetup will take place over at Jitsi. The Meetup will also be livestreamed to Youtube.

If someone would like to propose a talk or a topic, feel free to do so! We currently have no topics 😉

Mike Shah a computer science professor who teaches programming topics, primarily modern C++, C, D, game, and computer graphics. He is also a former senior 3D Graphics Engineer who worked at several game and graphics companies. He also has a YouTube channel where he covers a variety of software development topics with a focus on D and C++.

Over the past several months, he has been exploring several alternative high performance languages as part his First Impressions series, devoting a full episode to each one. Instead of giving a canned presentation, he lets the audience ride along on his journey as he tries to uncover the language's capabilities while sharing his impressions along the way.

His latest episode #16 covers Ada, which should be exciting after already covering 15 of them:

🛠 Ada first steps on ∞ Arduino Due!

Exciting news! 📖 The first four chapters of a new course "Advanced Journey With Ada: A Flight In Progress" are now available. Dive into topics like Data Types, Control Flow, Modular Programming, Resource Management and more. Download the PDF or EPUB 📦 or better read online 🌐 and try examples live in your browser 🔧!

In this webinar, Yannick Moy outlines key features of SPARK Pro, including demos on pointer ownership, function contracts and safe type casting.

Watch this session to learn more about:

• The rich possibilities for data representation in SPARK
• Available contracts on data types
• The ownership principle for tracking pointers to data
• Available contracts on functions
• Handling of bindings with C libraries, safe type casting, software-hardware interactions
• Specializing the analysis for a given target platform

🚀 pla-util, the power line adapter utility, is now part of Alire - your package manager for Ada!

Manage HomePlug AV2 compliant power line adapters like BCM60500 or BCM60333 effortlessly on Linux. Explore the capabilities with pla-util 2.1.1. Check out the commands, set configurations, and make the most of your power line adapters. 🛠️💡