Ivan Perez 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 and 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 on his work, which I think does an amazing job at showing how easy it is to get it running on arduinos.

Thanks Ivan. The talk was at Houston PFUG and is here: https://www.youtube.com/watch?v=l-luyVRgWVU I would love to see a talk explaining programming the Copilot DSL from someone who understands it better. :-) -- see shy jo

Karel Gardas wrote:

Thanks for the talk and for the arduino and zephyr support. However seen this I can't resist to think that you basically turn copilot upside down and make that a real "pilot". E.g. you turn all the sampling of system variables and comparing with the spec idea to let's make it a real C code and run that instead. Am I right or still not getting whole idea behind the Copilot?

Yes, the Arduino is being piloted without anyone in the other seat, as it were. arduino-copilot generates just enough C code to make that work, relying heavily on the arduino libraries. -- see shy jo

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