[Haskell-cafe] [ANN] Copilot 4.4

[Ivan Perez]

Hi everyone!!

We are really excited to announce Copilot 4.4 [1,2]. Copilot is a
stream-based EDSL in Haskell for writing and monitoring embedded C
programs, with an emphasis on correctness and hard realtime
requirements. Copilot is typically used as a high-level runtime
verification framework, and supports temporal logic (LTL, PTLTL and
MTL), clocks and voting algorithms. Compilation to Bluespec, to
target FPGAs, is also supported.

Copilot is NASA Class D open-source software, and is being used at NASA
in drone test flights. Through the NASA tool Ogma [3] (also written in
Haskell), Copilot also serves as a programming language and runtime
framework for NASA's Core Flight System, Robot Operating System (ROS2),
FPrime (the software framework used in the Mars Helicopter). Ogma now
supports producing flight and robotics applications directly in Copilot,
not just for monitoring, but for implementing the logic of the
applications themselves.

This release introduces several updates, bug fixes and improvements to
Copilot:

- The Kind2 backend is now able to distinguish between existentially and
  universally quantified properties.

- The fields of the existential record type Copilot.Core.Type.UType have
  now been removed.

- The build status icon in the README has now been corrected to show the
  current build status.

The new implementation is compatible with versions of GHC from 8.6 to
9.12.

This release has been made possible thanks to key submissions from Ryan
Scott (Galois) and Kyle Beechly, both recurrent contributors to Copilot.
We are grateful to them for their contributions, and for making Copilot
better every day.

For details on this release, see [1].

As always, we're releasing exactly 2 months since the last release. Our
next release is scheduled for July 7th, 2025.

We want to remind the community that Copilot is now accepting code
contributions from external participants again. Please see the
discussions and the issues in our github repo [4] to learn how to
participate.

Current emphasis is on using Copilot for full data processing
applications (e.g, system control, arduinos, rovers, drones), merging
stable features (i.e., visualizer, Bluespec backend, verifier) into the
mainline, improving usability, performance, and stability, increasing
test coverage, removing unnecessary dependencies, hiding internal
definitions, formatting the code to meet our new coding standards, and
simplifying the Copilot interface. Users are encouraged to participate
by opening issues, asking questions, extending the implementation, and
sending bug fixes.

Happy Haskelling!

Ivan

--

[1] https://github.com/Copilot-Language/copilot/releases/tag/v4.4

[2] https://hackage.haskell.org/package/copilot

[3] https://github.com/nasa/ogma

[4] https://github.com/Copilot-Language/copilot
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20250525/1b29f44f/attachment.html>