[ANN] Copilot 4.3

[ivanperez-keera]

Hi everyone!!

We are really excited to announce Copilot 4.3. 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 (@RyanGlScott) and Esther Conrad (@estherdconrad), 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.

We want to remind the community that Copilot is now accepting code contributions from external participants again. Please see the discussions and the issues to learn how to participate.

For details on this release, see: 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.

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!