[Haskell-cafe] ANN: Copilot 3.10

Richard O'Keefe raoknz at gmail.com
Sun Jul 17 13:13:26 UTC 2022

How hard would it be to use Copilot with ESP32 boards,
using their C SDK libraries for I/O?

The RPi Pico is also a candidate for the project we've just
submitted a grant proposal for.  The Pico has "PIO" and the
ESP32 chips have "ULP" and they are both basically very low
power finite state machines that can handle basic I/O while
the main CPU(s) is(are) dead to the world.

On Sat, 16 Jul 2022 at 21:50, Ivan Perez <ivanperezdominguez at gmail.com>

> > We also want to thank everyone who uses and helps promote
> > Copilot
> By the way, I'd like to give a shoutout to Joey Hess, who has built
> arduino-copilot <https://hackage.haskell.org/package/arduino-copilot> and
> zephyr-copilot <https://hackage.haskell.org/package/zephyr-copilot>. Joey
> updated both projects immediately after our release so that they work with
> Copilot 3.10.
> I've just found out that he also gave a talk
> <https://www.youtube.com/watch?v=l-luyVRgWVU> on his work, which I think
> does an amazing job at showing how easy it is to get it running on arduinos.
> Cheers,
> Ivan
> On Tue, 12 Jul 2022 at 07:43, Ivan Perez <ivanperezdominguez at gmail.com>
> wrote:
>> Dear all,
>> We are very happy to announce the release of Copilot 3.10. Copilot is a
>> runtime verification system implemented as a Haskell DSL that generates
>> hard-realtime C99. You can learn more about it at [1].
>> This new version of Copilot contains a small but important change in how
>> structs are handled in C functions invoked by the monitors when property
>> violations are detected. This change is API-breaking, so users of
>> Copilot may need to adapt their systems accordingly. The release also
>> contains a number of bug fixes, provides a simplified API, deprecates
>> outdated elements, removes unused code, and relaxes version constraints
>> for dependencies. A full list of changes merged is available at [2].
>> A substantial effort is being made to achieve NASA's Class D software
>> classification, most notably in terms of development process (which you
>> can partly witness in how issues and PRs are being handled on our github
>> repo), test coverage (mostly with quickcheck), and proofs of correctness
>> of the generated code (with what4).
>> Copilot is being used by the Safety-Critical Avionics Systems Branch
>> (D320) of NASA Langley Research Center to conduct experiments related to
>> flight safety of aerial vehicles. We have also built Ogma [3], a tool
>> that allows us to generate full monitoring applications (e.g., NASA's
>> Core Flight System [4] applications) from requirements in structured
>> natural language.
>> We'd like to take this opportunity to welcome Will Pogge to the team
>> with his first commit, and thank the Galois team for their
>> contributions. We also want to thank everyone who uses and helps promote
>> Copilot; we are seeing increased attention, and gave three talks in the
>> last two months at JPL, USC, and VCU, with two more taking place this
>> month.
>> We invite you all to explore Copilot, to try it, and to extend it. If
>> you like it, please help us draw attention to this work with a star on
>> github or a mention online.
>> Happy Haskelling,
>> The Copilot Team
>> [1] https://github.com/Copilot-Language/copilot
>> [2] https://github.com/Copilot-Language/copilot/milestone/14?closed=1
>> [3] https://github.com/nasa/ogma
>> [4] https://cfs.gsfc.nasa.gov/
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220718/38804cfa/attachment.html>

More information about the Haskell-Cafe mailing list