Copilot: Realtime programming language and runtime verification framework | Hacker News Reader

Copilot: Realtime programming language and runtime verification framework

copilot-language.github.io

145 pointsducktective63 comments

I post this every time this comes by: if you ever find yourself needing to (or more realistically, wanting to) write your own hard realtime programs but don't have a NASA-grade drone to play with, check out the arduino-copilot library by Joey Hess. I wrote a blog post about it at https://wjwh.eu/posts/2020-01-30-arduino-copilot.html :)

This framework claims it can generate a C code that is constant-time and constant-size (awesome!). However, in their manual [1], in section 4.1, it does not take into account that low-level C functions `heaton` and `heatoff` may fail since both of them are returning `void`.

Like if we should increase the temp, we can tolerate a couple of heaton fails before it reaches to some min limit.

[1]: https://copilot-language.github.io/downloads/copilot_tutoria...

in this sort of scenario you would detect the error by a failure to see an increase in temperature over some interval.

the trigger functions typically would just raise dio lines high which is not something that really fails unless you're completely crashed.

Is it actually a given that these C functions could fail? It is certainly not apparent from their function signatures, as you already mention. :) If it just writes to some memory mapped I/O registers then it might well not be possible to fail that (unless writing memory in general has become impossible, but at that time no software will save you anymore).

In any case let's not judge the writers too harshly for omitting some error checking in the very first complete example they provide in the manual. The typical introductory "hello world" program also doesn't contain error handling to check if writing to stdout succeeded or not. A real CoPilot program could (and should!) have a separate stream for checking `heaterStatus` and raise a separate alarm if the status of the heater does not update when it should.

>it just writes to some memory mapped I/O registers

Yes but the heater is a mechanical device that behaves unexpectedly. I mean, should the "fault-tolerance" logic be handled in the copilot DSL itself?

Checking if the heater is working is a different task than telling the heater what to do. You can't fail to tell the heater what to do. However, it's your job as the programmer to make sure the heater is doing what it's supposed to.

Last I checked it was a run loop with a delay and it didn't support low power mode :( But otherwise it looks great.

FYI if any Copilot maintainers come across this comment, the link to the examples on this page is broken : https://copilot-language.github.io/documentation.html

not maintainer but I think the correct one is this: https://github.com/Copilot-Language/copilot/tree/master/copi...

Correct link appears to be

https://github.com/Copilot-Language/copilot/tree/master/copi...

There are so many programming languages to collect temperature readings.

In case you are wondering which copilot came first (I certainly was) - this repository starts in 2010 with a source code upload: https://github.com/Copilot-Language/copilot/commits/b2fc3456...

But unfortunately for them “Copilot” in 2022 means GH Copilot.

Words sometimes having two meanings has been alluded to in the literature as early as 1971.

I think we had metaphors before that?

Am I missing a joke here or something? Surely people knew about homonyms prior to 1971

We knew about them, but we didn't talk about it.

https://en.m.wikipedia.org/wiki/Stairway_to_Heaven

Which is itself a name collision with an earlier Neil Sedaka song.

This page makes no reference to any synonyms. Can you explain?

The lyrics of the song include: “sometimes words have two meanings”

Lyrics:

And she's buying a stairway to heaven There's a sign on the wall But she wants to be sure 'Cause you know, sometimes words have two meanings

Unfortunately for Joel Spolsky / Fog Creek Copilot[1] remote control tool from ~2005, and for people who fly aeroplanes[2] from 1933.

[1] https://www.joelonsoftware.com/2007/01/26/copilot-20-ships/

[2] https://www.etymonline.com/word/copilot

I have not looked further but this looks like Haskell. I see haskell, I upvote.

Any tool that is PL-related has a good chance of being implemented by functional programmers who then inject their syntactic preferences into the tool itself.

There are a lot of type-level checks you can do in Haskell that are simply not feasible in most other languages and that helps with the realtime guarantees of the generated code. Syntactic preferences may also be there of course (Haskell is certainly not underrepresented in compiler dev circles), but there are definitely technical reasons as well.

Can you expound on how Haskell's type-level checks can help with realtime guarantees of generated code?

In a nutshell, most languages allow their functions/methods to do almost everything by default. My Ruby methods can log to stdout, mutate global state, create files on disk, truncate database tables, throw exceptions, fire the missiles and generally do whatever it wants. The default is very permissive. The most basic Haskell function on the other hand can do almost nothing. It can access nothing except it's (immutable) arguments and do nothing except returning a result. If you want to add more 'functionality' to it, you have to explicitly mention that in its type. The typical way to do that in Haskell is to add one or more monadic contexts to it. Writing to a file would typically require access to the the `IO` context for example, and if a function does not have that then file I/O would be a compiler error.

To bring it back to CoPilot, it is a heavily restricted DSL where all variables are streams of values, each of which gets updated in every iteration of the main loop. The types of the functions and datatypes that you can manipulate these streams with don't contain any "interesting" monadic contexts, so you definitely can't access the outside world other than through the provided interfaces. You are also mostly restricted to mathematical operations on these streams, like summing or multiplying two other streams to produce a third stream. This already restricts a lot of the variability you could introduce in a "normal" program. The CoPilot project then contains a dedicated Haskell-to-C compiler that will try its best to generate constant-time and constant-memory code. If that is not possible, it will generate a compiler error indicating which part was not possible to compile in such a way. For example, for most recursive functions it would not be possible to prove it terminates in a predictable amount of time so that would be right out.

Of course, even if it does compile then there are no guarantees that the code will fit inside your time or memory budget. It is still possible to write code that is inefficient or contains bugs. It will just always take the same amount of memory and same amount of cycles per iteration.

Thanks a lot, I really appreciate your explanation.

Okay, so this is a DSL embedded in Haskell. I thought Copilot was a standalone language with a Haskell-like syntax.

From the Download page[1]:

> Copilot is implemented as a Embedded Domain Specific Language in Haskell. Currently Copilot 3.1 requires a version of the Glasgow Haskell Compiler (GHC) of at least 8.0 to be installed.

So yeah, looks like Haskell because it is Haskell! :)

[1]: https://copilot-language.github.io/download.html

I would love it if we could have HN threads where we're not discussing the naming of things, nor complaining about the discussion of naming of things like I am doing now.

That’s why there are multiple threads. The real problem is that people are bringing up this same issue in a dozen top level comments.

Threads and naming things, two famously easy problems.

In this particular case it’s helpful, as the link is to github.

Naming things is hard. I submit that as a core tenet of the software industry, we will discuss the naming of things so long as there are things to discuss.

Naming things uniquely with common words is hard.

Good names like Linux, Google, Kodak, Adidas, etc are instantly recognizable and cannot be mistaken for anything else.

Availability of a domain name might be a good proxy for how recognizable a name is. Well, maybe it was up until 2008 or so.

This is not the same as Github Copilot.

or AWS copilot

not the Copilot app either, oof

Possibly could be used to write an automated co-pilot though.

Nor Performance Co-Pilot (PCP), sometimes abbreviated as just "co-pilot".

Which in turn hopefully has nothing to do with Phencyclidine(PCP)

But mashing this to github copilot would be my personal dream come true.

Once again the one of the hardest problems in software engineering is naming things.

Is it a bad name?

It clashes with the AI code writing tool of the same name.

Which came first?

The egg.

This predates the AI thing by years.

Then the AI code writing tool should be criticized instead.