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.
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.
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.
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.
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.
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.
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.
> 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! :)
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.
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?
73 comments
[ 2.5 ms ] story [ 158 ms ] threadAnd 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
[1] https://www.joelonsoftware.com/2007/01/26/copilot-20-ships/
[2] https://www.etymonline.com/word/copilot
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...
the trigger functions typically would just raise dio lines high which is not something that really fails unless you're completely crashed.
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.
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?
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
Good names like Linux, Google, Kodak, Adidas, etc are instantly recognizable and cannot be mistaken for anything else.
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.
> 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
https://github.com/Copilot-Language/copilot/tree/master/copi...
I hate to say it.
This is something that actually, genuinely should, be re-written in Rust.
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.
Should its author generate Rust from Rust? Would it be better if Copilot produced object files or executables directly, or used eg. LLVM IR?