Copilot: Realtime programming language and runtime verification framework(copilot-language.github.io)
copilot-language.github.io
Copilot: Realtime programming language and runtime verification framework
https://copilot-language.github.io/
73 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 :)
Last I checked it was a run loop with a delay and it didn't support low power mode :(
But otherwise it looks great.
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...
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...
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.
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?
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.
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.
the trigger functions typically would just raise dio lines high which is not something that really fails unless you're completely crashed.
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
Correct link appears to be
https://github.com/Copilot-Language/copilot/tree/master/copi...
https://github.com/Copilot-Language/copilot/tree/master/copi...
not maintainer but I think the correct one is this: 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.
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
[1] https://www.joelonsoftware.com/2007/01/26/copilot-20-ships/
[2] https://www.etymonline.com/word/copilot
Words sometimes having two meanings has been alluded to in the literature as early as 1971.
Am I missing a joke here or something? Surely people knew about homonyms prior to 1971
Which is itself a name collision with an earlier Neil Sedaka song.
We knew about them, but we didn't talk about it.
I think we had metaphors before that?
[deleted]
I have not looked further but this looks like Haskell. I see haskell, I upvote.
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
> 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
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.
Okay, so this is a DSL embedded in Haskell. I thought Copilot was a standalone language with a Haskell-like syntax.
[deleted]
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.
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.
[deleted]
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.
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.
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.
In this particular case it’s helpful, as the link is to github.
[deleted]
This is not the same as Github Copilot.
But mashing this to github copilot would be my personal dream come true.
or AWS copilot
not the Copilot app either, oof
Nor Performance Co-Pilot (PCP), sometimes abbreviated as just "co-pilot".
Which in turn hopefully has nothing to do with Phencyclidine(PCP)
[deleted]
Possibly could be used to write an automated co-pilot though.
[deleted]
Once again the one of the hardest problems in software engineering is naming things.
Solved by namespaces
Is it a bad name?
See also: Meta
Lots of things predate Meta (Facebook) and Copilot (Microsoft), but the new thing muscled its way in and now anything that already had those names will struggle.
https://www.youtube.com/watch?v=-4spxWgms1c
Lots of things predate Meta (Facebook) and Copilot (Microsoft), but the new thing muscled its way in and now anything that already had those names will struggle.
https://www.youtube.com/watch?v=-4spxWgms1c
A recent stack overflow bikeshed asked why Firefox refers to it's UI elements by the name of Google's browser.
It clashes with the AI code writing tool of the same name.
This predates the AI thing by years.
Then the AI code writing tool should be criticized instead.
[deleted](1)
[deleted]
> Copilot 3.9, a stream-based DSL for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements.
I hate to say it.
This is something that actually, genuinely should, be re-written in Rust.
I hate to say it.
This is something that actually, genuinely should, be re-written in Rust.
The software is written in Haskell. I don't know much about it but it doesn't look like a bad choice. Remember that it is just a compiler / test tool, it is not the embedded part, that would be the target. I don't think Rust brings much to the table here.
It uses C as a back end, which is a sensible thing to do since it is the default in embedded software development, few embedded toolchains support Rust. And it is just a backend, they could have output machine code directly, but C is more universal and you can take advantage of all the C compiler optimizations. Using Rust for this would get you all of the disadvantages and none of the advantages that Rust has over C.
Now, maybe you mean writing embedded code in Rust instead of C, at least, now you have a point, Rust has features that I think would be well suited for critical embedded software. But that's also what Copilot tries to do, if anything, Copilot competes against Rust (and ADA). I say that in the sense that they all address the same problem (safety) and you have to choose one solution, not that they are enemies.
It uses C as a back end, which is a sensible thing to do since it is the default in embedded software development, few embedded toolchains support Rust. And it is just a backend, they could have output machine code directly, but C is more universal and you can take advantage of all the C compiler optimizations. Using Rust for this would get you all of the disadvantages and none of the advantages that Rust has over C.
Now, maybe you mean writing embedded code in Rust instead of C, at least, now you have a point, Rust has features that I think would be well suited for critical embedded software. But that's also what Copilot tries to do, if anything, Copilot competes against Rust (and ADA). I say that in the sense that they all address the same problem (safety) and you have to choose one solution, not that they are enemies.
I meant the embedded C back-end, yes. Rewriting the Haskell DSL doesn't really make sense.
This alternative Rust compiler's intermediate representation is C code, which is then run through another compiler to produce the final output: https://github.com/thepowersgang/mrustc
Should its author generate Rust from Rust? Would it be better if Copilot produced object files or executables directly, or used eg. LLVM IR?
Should its author generate Rust from Rust? Would it be better if Copilot produced object files or executables directly, or used eg. LLVM IR?
Don’t think anyone would stop you…
Rust, the one true programming language that will save us all. Repent! and confess your sins so that Rust may have mercy upon your soul.
Rust is the legit the best thing that has happened to the industry in the last 30 years.
- looks for rust jobs
- finds none