[HN Gopher] Copilot: Realtime programming language and runtime v...
___________________________________________________________________
Copilot: Realtime programming language and runtime verification
framework
Author : ducktective
Score : 119 points
Date : 2022-08-25 16:38 UTC (2 days ago)
(HTM) web link (copilot-language.github.io)
(TXT) w3m dump (copilot-language.github.io)
| jesse__ wrote:
| 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
| ducktective wrote:
| not maintainer but I think the correct one is this:
| https://github.com/Copilot-Language/copilot/tree/master/copi...
| mmastrac wrote:
| Correct link appears to be
|
| https://github.com/Copilot-Language/copilot/tree/master/copi...
| zitterbewegung wrote:
| Once again the one of the hardest problems in software
| engineering is naming things.
| dqpb wrote:
| Solved by namespaces
| keybored wrote:
| Is it a bad name?
| atty wrote:
| It clashes with the AI code writing tool of the same name.
| keybored wrote:
| Then the AI code writing tool should be criticized instead.
| fnfjcu7 wrote:
| Which came first?
| dotancohen wrote:
| The egg.
| wyager wrote:
| This predates the AI thing by years.
| Kye wrote:
| 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
| dotancohen wrote:
| A recent stack overflow bikeshed asked why Firefox refers
| to it's UI elements by the name of Google's browser.
| [deleted]
| [deleted]
| TheDesolate0 wrote:
| vouaobrasil wrote:
| This is not the same as Github Copilot.
| [deleted]
| antupis wrote:
| But mashing this to github copilot would be my personal dream
| come true.
| andridk wrote:
| or AWS copilot
| obert wrote:
| not the Copilot app either, oof
| bongobingo1 wrote:
| Possibly could be used to write an automated co-pilot
| though.
| capableweb wrote:
| Nor Performance Co-Pilot (PCP), sometimes abbreviated as
| just "co-pilot".
| mtlmtlmtlmtl wrote:
| Which in turn hopefully has nothing to do with
| Phencyclidine(PCP)
| [deleted]
| toomanydoubts wrote:
| I have not looked further but this looks like Haskell. I see
| haskell, I upvote.
| [deleted]
| _rend wrote:
| 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
| keybored wrote:
| 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.
| WJW wrote:
| 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.
| heavyset_go wrote:
| Can you expound on how Haskell's type-level checks can help
| with realtime guarantees of generated code?
| WJW wrote:
| 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.
| keybored wrote:
| Okay, so this is a DSL embedded in Haskell. I thought
| Copilot was a standalone language with a Haskell-like
| syntax.
| [deleted]
| WJW wrote:
| 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 :)
| ducktective wrote:
| 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...
| a-dub wrote:
| 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.
| WJW wrote:
| 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.
| ducktective wrote:
| >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?
| urthor wrote:
| > 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.
| GuB-42 wrote:
| 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.
| UncleEntity wrote:
| Don't think anyone would stop you...
| wudangmonk wrote:
| 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.
| adamnemecek wrote:
| Rust is the legit the best thing that has happened to the
| industry in the last 30 years.
| Bellend wrote:
| - _looks for rust jobs_ - _finds none_
| datalopers wrote:
| There are so many programming languages to collect temperature
| readings.
| mmastrac wrote:
| 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.
| MattRix wrote:
| 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.
| markrages wrote:
| Threads and naming things, two famously easy problems.
| plugin-baby wrote:
| In this particular case it's helpful, as the link is to github.
| [deleted]
| dotancohen wrote:
| 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.
| nine_k wrote:
| 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.
| [deleted]
| rzzzt wrote:
| 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...
| [deleted]
| p1esk wrote:
| But unfortunately for them "Copilot" in 2022 means GH Copilot.
| jodrellblank wrote:
| 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
| pvg wrote:
| Words sometimes having two meanings has been alluded to in
| the literature as early as 1971.
| lowdose wrote:
| I think we had metaphors before that?
| spencerchubb wrote:
| Am I missing a joke here or something? Surely people knew
| about homonyms prior to 1971
| mbg721 wrote:
| We knew about them, but we didn't talk about it.
| markrages wrote:
| https://en.m.wikipedia.org/wiki/Stairway_to_Heaven
| elcomet wrote:
| This page makes no reference to any synonyms. Can you
| explain?
| memalign wrote:
| The lyrics of the song include: "sometimes words have two
| meanings"
| Jorge1o1 wrote:
| 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
| kej wrote:
| Which is itself a name collision with an earlier Neil
| Sedaka song.
___________________________________________________________________
(page generated 2022-08-27 23:00 UTC)