<div dir="ltr"><div class="gmail_default" style="font-family:monospace,monospace">How hard would it be to use Copilot with ESP32 boards,</div><div class="gmail_default" style="font-family:monospace,monospace">using their C SDK libraries for I/O?</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace" class="gmail_default">The RPi Pico is also a candidate for the project we've just</div><div style="font-family:monospace,monospace" class="gmail_default">submitted a grant proposal for.  The Pico has "PIO" and the</div><div style="font-family:monospace,monospace" class="gmail_default">ESP32 chips have "ULP" and they are both basically very low</div><div style="font-family:monospace,monospace" class="gmail_default">power finite state machines that can handle basic I/O while</div><div style="font-family:monospace,monospace" class="gmail_default">the main CPU(s) is(are) dead to the world.</div><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 16 Jul 2022 at 21:50, Ivan Perez <<a href="mailto:ivanperezdominguez@gmail.com">ivanperezdominguez@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span><span><span dir="ltr">> We also want to thank everyone who uses and helps promote<br></span></span></span><div><span><span><span dir="ltr"><span>> Copilot</span></span></span></span></div><div><span><span><span dir="ltr"><span><br></span></span></span></span></div><div><span><span><span dir="ltr"><span>By the way, I'd like to give a shoutout to Joey Hess, who has built </span></span></span></span><span><span><span dir="ltr"><span></span></span></span></span><a href="https://hackage.haskell.org/package/arduino-copilot" target="_blank"><span><span><span dir="ltr"><span>arduino-copilot</span></span></span></span></a><span><span><span dir="ltr"><span> and <a href="https://hackage.haskell.org/package/zephyr-copilot" target="_blank">zephyr-copilot</a>. Joey updated both projects immediately after our release so that they work with Copilot 3.10.<br></span></span></span></span></div><div><span><span><span dir="ltr"><span><br></span></span></span></span></div><div><span><span><span dir="ltr"><span>I've just found out that he also gave <a href="https://www.youtube.com/watch?v=l-luyVRgWVU" target="_blank">a talk</a> on his work, which I think does an amazing job at showing how easy it is to get it running on arduinos.<br></span></span></span></span></div><div><span><span><span dir="ltr"><span><br></span></span></span></span></div><div><span><span><span dir="ltr"><span>Cheers,</span></span></span></span></div><div><span><span><span dir="ltr"><span><br></span></span></span></span></div><div><span><span><span dir="ltr"><span>Ivan<br></span></span></span></span></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 12 Jul 2022 at 07:43, Ivan Perez <<a href="mailto:ivanperezdominguez@gmail.com" target="_blank">ivanperezdominguez@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><span><span><span dir="ltr">Dear all,</span></span></span></div><div><span><span><span dir="ltr"><br></span></span></span></div><div><span><span><span dir="ltr">We are very happy to announce the release of Copilot 3.10. Copilot is a<br>runtime verification system implemented as a Haskell DSL that generates<br>hard-realtime C99. You can learn more about it at [1].<br><br>This new version of Copilot contains a small but important change in how<br>structs are handled in C functions invoked by the monitors when property<br>violations are detected. This change is API-breaking, so users of<br>Copilot may need to adapt their systems accordingly. The release also<br>contains a number of bug fixes, provides a simplified API, deprecates<br>outdated elements, removes unused code, and relaxes version constraints<br>for dependencies. A full list of changes merged is available at [2].<br><br>A substantial effort is being made to achieve NASA's Class D software<br>classification, most notably in terms of development process (which you<br>can partly witness in how issues and PRs are being handled on our github<br>repo), test coverage (mostly with quickcheck), and proofs of correctness<br>of the generated code (with what4).<br><br>Copilot is being used by the Safety-Critical Avionics Systems Branch<br>(D320) of NASA Langley Research Center to conduct experiments related to<br>flight safety of aerial vehicles. We have also built Ogma [3], a tool<br>that allows us to generate full monitoring applications (e.g., NASA's<br>Core Flight System [4] applications) from requirements in structured<br>natural language.<br><br>We'd like to take this opportunity to welcome Will Pogge to the team<br>with his first commit, and thank the Galois team for their<br>contributions. We also want to thank everyone who uses and helps promote<br>Copilot; we are seeing increased attention, and gave three talks in the<br>last two months at JPL, USC, and VCU, with two more taking place this<br>month.<br><br>We invite you all to explore Copilot, to try it, and to extend it. If<br>you like it, please help us draw attention to this work with a star on<br>github or a mention online.<br><br>Happy Haskelling,<br>The Copilot Team<br></span></span></span></div><div><br><span><span><span dir="ltr"></span></span></span></div><div><span><span><span dir="ltr"></span></span></span></div><div><span><span><span dir="ltr">[1] <span><span><span dir="ltr"><a href="https://github.com/Copilot-Language/copilot" target="_blank">https://github.com/Copilot-Language/copilot</a></span></span></span></span></span></span></div><div><span><span><span dir="ltr"><span><span><span dir="ltr">[2] <span><span><span dir="ltr"><a href="https://github.com/Copilot-Language/copilot/milestone/14?closed=1" target="_blank">https://github.com/Copilot-Language/copilot/milestone/14?closed=1</a></span></span></span></span></span></span></span></span></span></div><div><span><span><span dir="ltr"><span><span><span dir="ltr"><span><span><span dir="ltr">[3] <a href="https://github.com/nasa/ogma" target="_blank">https://github.com/nasa/ogma</a></span></span></span></span></span></span></span></span></span></div><div><span><span><span dir="ltr"><span><span><span dir="ltr"><span><span><span dir="ltr">[4] <a href="https://cfs.gsfc.nasa.gov/" target="_blank">https://cfs.gsfc.nasa.gov/</a></span></span></span></span></span></span></span></span></span></div></div>
</blockquote></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>