[Haskell-cafe] [ANN] Copilot 4.3

[Ivan Perez]

Hi everyone!!

We are really excited to announce Copilot 4.3 [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 runtime monitoring backend for
NASA's Core Flight System, Robot Operating System (ROS2), FPrime (the
software framework used in the Mars Helicopter).

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

- Specifications now produce information about counterexamples when
  copilot-theorem is able to prove the property false.

- We introduce a new Prop construct in copilot-core that captures the
  quantifier used in a property.

- The What4 backend of Copilot theorem now produces an exception when
  trying to prove an existential property. The restriction of not being
able to handle existentially quantified properties already existed, but
due to information loss during the reification process, the quantifier
was being lost and all properties to be proved via what4 were being
treated as a universally quantified.

- Several deprecated functions have been removed.

- The installation instructions have been updated.

- Compatibility with GHC 9.10 is now explicitly listed in the README.

- Several typos have been fixed in comments and documentation.

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

This release has been made possible thanks to key submissions from Ryan
Scott (Galois) and Esther Conrad (NASA), the last of which is also a
first-time contributor to the project. We are grateful to them for
their timely contributions, especially during the holidays, and for
making Copilot better every day.

For details on this release, see [1].
https://github.com/Copilot-Language/copilot/releases/tag/v4.3.

As always, we're releasing exactly 2 months since the last release. Our
next release is scheduled for May 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), 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.3

[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/20250317/30feeef3/attachment.html>