[Haskell-cafe] ANN: Copilot 3.10

[Richard O'Keefe]

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>
wrote:

> > 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>