9 ms·

The future of programming with certified program synthesis

84 points by tluyben2 5y ago

dataflow 5y ago
Looks great. One question though (and this isn't criticism of the research, but just about the presentation/intended audience): why would anyone who's been so 'stubborn' (as they say) so far about sticking with C finally have a change of heart because of this? They clearly prefer to write C themselves, otherwise they'd have already moved on, right? It's not like having a C++-to-C or Rust-to-C compiler would've changed the game for them.
- tluyben2 5y ago
  (not one of researchers but I submitted this because I like the research) I have not tried Rust for a while so this might have changed, but in the tiny embedded devices I work in, where your 'free' memory is for instance 24kb and the speed of the MCU is a few mhz, there really is only C/asm. You need to mess around with every single byte to make it fit and fast enough. There are surprisingly many of these MCU's around everywhere around us. And you (usually) cannot update their firmware remotely (or at all actually), so it's important it doesn't have massive bugs.
  - dataflow 5y ago
    People say this all the time, and maybe it's just my naivete, but I just don't understand why at least something like C++ is not an option in embedded spaces. Sure you might need to avoid operator new() and exceptions or whatever, but you still have so much more power than in plain C even with half the language removed, and avoid so many of the C pitfalls just by that. I know people kept telling me you "need" C for a kernel... and I just ignored them and wrote drivers and even a basic from-scratch kernel in C++, and they all worked just fine, and with so much less pain than C. And honestly, if C++ somehow (I don't understand how, but let's say somehow) has too much overhead... why would another language compiled to C be any better? It just doesn't make sense to me.
    - Animats 5y ago
      You can use C++ on even an Arduino. In fact, the Arduino development development is full C++. You just have to stick to the non-Clib features.
    - tluyben2 5y ago
      C++ is no issue but, to make very small binaries packed with the features we need, you need a lot of fiddling and the end it does not look like c++. Not to mention that most embedded devs (at least in Asian, Africa and eu embedded corps which make deployments of millions of mcu's, not home arduino users: there might be more of those) work mostly with C. I think most are waiting to skip a revolution to something like Rust but that does not fit yet. So this solution gives at least some handles to add verification. That said, there are more of these projects. I think there is an F* project too. > why would another language compiled to C be any better? It just doesn't make sense to me. It seems that the formalization in the article allows for very low level operation which you would use in C while not writing C. As said, sure you can do that in C++ but then you gain little or nothing. I have not tried this, only posted it because I would like for something robust like it to exist. Now we use Coq (or more recent idris) to write things and hand translate them to mcu asm/c.
  - pjmlp 5y ago
    Not really, there are options available for those that care to look around. https://www.mikroe.com/mikropascal https://www.mikroe.com/mikropascal https://www.mikroe.com/mikrobasic https://www.mikroe.com/mikrobasic Mikroe is just one possible vendor, there are others.
    - tluyben2 5y ago
      Sure, you can: Forth works too. But C is the standard (in my world anyway) so it would be c++ or rust. C++ already is used but Rust I have not seen yet.
      - pjmlp 5y ago
        Sure but you worded it as universal condition, hence my remark. If anything, just to raise awareness for others. Even C++ alone is already an improvement, provided it isn't just C compiled with a C++ compiler, e.g. AUTOSAR.
        tluyben2 5y ago
        Yep, I agree but we never could make that fit. When it fit, it was just compiled with a c++ compiler pretty much. But I have not met an experienced c++ embedded dev in my industries: all are c/asm because it is always the cheapest (and thus most underpowered) we can get away with given the consumption demands.
  - kaba0 5y ago
    Messing around with every single byte is a property of low-level languages. There is absolutely nothing C does differently than C++ or Rust. Hell, it may even be slower due to not having proper abstraction powers and programmers thus lazily choose the easier route with eg. linked lists. Also, due to rust’s semantics it can get better optimizations due to no pointer aliasing.
    - tluyben2 5y ago
      I will try it again then. What is your experience with it in very small devices? As I read online still, the binaries would not fit in the mcus we use. Maybe I am missing something there which has changed or I just missed. I would love to see a realistic (not hello world) example on a 32kb mcu. So with significant amount of function points (we do decryption, signing, otp generation, display driver, keyboard, and lot more and people told me and I read online this would not work well with Rust but this is maybe outdated or maybe the code will just look like C? I don't know examples of anything realistic): think that would turn me and more people.
      - kaba0 5y ago
        If binary size is that important, then there is even better options than C: Zig.
        tluyben2 5y ago
        Well, every 0.01$ counts for these components as orders are in the millions or 10s of millions. Everything that can be cut gets cut. And now lead times count as well as there are shortages and some factories have many waifers of these low spec ones to sell. I tried Zig on Linux and it is nice: any restricted embedded examples? I will try both Rust and zig when I get home to see if it could even work.
  - gradschool 5y ago
    Devil's advocate question for a person who likes this research: What formal definition of a "program synthesizer" would exclude C compilers from being program synthesizers? Similarly, what precisely distinguishes C or any other programming language from a "specification" language?
makerofthings 5y ago
That example they use to show how bad C code is and how complicated pointers can be. That’s just bad C, really bad. And how do I know if he removed a line? You could ask the same question about code in any language.
- tluyben2 5y ago
  The example is called listcopy, so assuming it does that, I don't think there are many modern languages where you could remove a line and have other (experienced) programmers not pick up on that. Unless that line had nothing to do with the actual task, but that's not the case here. Agreed it is bad code though. A good C example and then synthesised code of the same task would have been better imho.
  - comex 5y ago
    > The example is called listcopy, so assuming it does that, I don't think there are many modern languages where you could remove a line and have other (experienced) programmers not pick up on that. Thing is, if the hypothesis is that the complexities of pointers make C harder to read than other languages, this example does not prove that, because its use of pointer features is completely gratuitous. Below I attempted to write a saner version of the same C function. I removed the pointer arithmetic and casts in favor of just using a struct, not because I wanted to avoid those features for demonstration purposes, but because that's what any sane C code would do. I also changed it from accepting a pointer-to-pointer, where the pointee is originally the input value and is then replaced with the output value, to just taking the input as an argument and returning the output – again, because that's the simple and obvious choice. As it happens, the resulting code's use of pointers is limited enough that it could be directly transliterated to Java or any other high-level imperative language. Change the `malloc` to a `new`, fix up the syntax, and you're done. Therefore, whatever lack of clarity remains, it can't be due to anything peculiar to C. (I'd say at this point that the code is clear enough that most people would notice if you removed a line, but YMMV. To be fair, my version also shares some flaws with the original such as not checking for allocation failure.) That said, there are plenty of algorithms which are complex or subtle enough that even in a well-written implementation, someone might not notice a line being removed. But that can happen in any language, at least to some extent. struct list { int value; struct list *next; }; struct list * listcopy(struct list *list) { if (list != NULL) { struct list *copied = malloc(sizeof(*list)); copied->value = list->value; copied->next = listcopy(list->next); return copied; } else { return NULL; } }
rustybolt 5y ago
When I first read the snippet, I thought "What a terrible piece of code.". Later on, I read: "In fact, the code written above was actually entirely automatically synthesised by our tool, along with a proof certificate, formally guaranteeing its correctness." So it looks like the code is terrible, and they only give an example for a simple usecase. So I'm not very enthousiastic about using this technique in practice. The rest of the post looks very informative though, although I haven't completely read it yet.
- zozbot234 5y ago
  > So it looks like the code is terrible, and they only give an example for a simple usecase. Yes, I'm very skeptical about this being "the future of coding!" (quoting the OP). These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. Typically, a developer has to step in and provide the right invariant so that the tool can get unstuck. Proof synthesis has exact the same issue, so generating proof-carrying code is also something that cannot thus far be automated except in very simple cases. Having said that, separation logic can be a valuable low-level tool and has been used to assess the correctness of, e.g. Rust borrow checking, which aims to provide lightweight, composable guarantees that can scale up to encompass larger programs. Even there though, we're nowhere near an actual proof, and soundness issues have in fact cropped up in the past as new features got added.
  - YeGoblynQueenne 5y ago
    >> These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. By "inductive hypothesis" do you mean the inductive case in a recursion? If so, I'm curious, why do you say this? My experience is that the problem with learning recursion is constructing the "base case", particuarly when there is no example of it. Do you have specific examples where the inductive case is hard to find when learning from specifications?
shannongreen 5y ago
As someone who has to write C for their day job, I am a little bit offended by the introduction of this article, but I guess that's the point. The code presented is trash and doesn't follow best practices - using the type system, descriptive variable names, etc. Void pointers for everything, are you serious? Of course it's hard to understand. Revealing that it's the generated code doesn't make me any more comfortable with it. Yes, I get that you shouldn't care what the generated code looks like if you trust your input, but I don't find the predicate any easier to understand. How do I know that's correct? What if I need to debug this generated output?
- pjmlp 5y ago
  I have seen code written like that by humans, namely offshored projects.
- dang 5y ago
  I've taken "Goodbye C developers" out of the title above, since it's pretty linkbaity.
fjfaase 5y ago
The code snippet is incorrect. I do not see a check on malloc returning null. In general that would be okay, but in an embedded environment with limited memory, that would be a serious problem. Also, using recursion is bad, because copying a long list will lead to a stack overflow.
- omnicognate 5y ago
  It's never OK. Machines with lots of memory run out of memory too. To present a piece of research in such trollish terms, accusing "stubborn C developers" of causing security vulnerabilities, and then present an example of code for which "we didn't even have to bother reasoning about how exactly it did its pointer manipulations" that segfaults if it runs out of memory (it dereferences the result of malloc and writes to that location 2 lines down) is beyond hilarious.
  - bestouff 5y ago
    On Linux machines malloc()'s returning NULL doesn't mean you're out of memory, it means you're out of address space which is very different.
    - fjfaase 5y ago
      If I understand it correctly, it is even worse, because malloc could return not NULL and still throw an exception when you try to write to the 'allocated' memory. See for example https://linuxembedded.fr/2020/01/overcommit-memory-in-linux https://linuxembedded.fr/2020/01/overcommit-memory-in-linux
    - omnicognate 5y ago
      In a system with virtual memory there are a variety of limits you can hit that will prevent your process allocating more memory and cause malloc to return zero. It's normal to informally lump all these together as "running out of memory" when the distinction doesn't matter, as here. Address space size is one of these limits, not the only one. Hitting it is rare on 64-bit operating systems, common on 32-bit ones.
pjmlp 5y ago
Every tool is welcomed for the scenarios where there is no workaround as to keep writing C code, but for everything else, the best is not to write it to start with. In any case very interesting paper, however I feel such kind of tooling can only be enforced in scenarios where code certification is already taking place, e.g. MISRA and AUTOSAR.
Animats 5y ago
OK, so you write pre and post conditions for a function, and the function gets generated. OK, so now we're programming at the specification level. I've written formal specifications for an operating system. They're harder to write than code for non-trivial programs. Some things are trivial to specify but hard to code. A hash table, for example. It's easy to specify what a hash table does, but that gives no guidance on how to implement one. You might get out something that does a linear search. File systems and databases are similarly not too hard to specify - the specification describes the abstract brute-force approach. They need to get much further along before announcing victory.
- vidarh 5y ago
  You indirectly get at an important point: A complete specification must include best/worst/anortised performance constraints, and a lot of other details we often leave unstated. And then it gets a lot harder...
  - qayxc 5y ago
    A complete specification also must include assumptions about external systems and limits. Here the assumptions are infinite stack (or item count < stack size limit) and a malloc that never fails. Incomplete specs are just as bad as buggy code. I'd even argue that incomplete specs are worse in this scenario, because the "proven correctness" gives a false sense of security.
  - amw-zero 5y ago
    Performance is not a part of behavior. Specification is about specifying logical behavior and that's it. I don't know of any specification framework that supports saying anything about performance.
- dexen 5y ago
  In programming, coding is a tool for discovering the under-specified parts of the specification.
- YeGoblynQueenne 5y ago
kazinator 5y ago
> a simple, standard, procedure to copy a linked list: Using the same argument for the input and output, when making a copy, is idiotic, not standard. Well, maybe idiotic is standard, but that's another discussion. Copying linked lists is not a widespread practice in C programs, by the way; if we don't count C programs that are Lisp interpreters. It creates memory handling problems. In this example, the nodes carry data consisting of integer values. These are referenced by pointers. The copy is shallow-copying these pointers, which could be an issue. If the integers are dynamically allocated, who cleans them up? They have to persist as long as either list is still reachable. The average embedded C programmer's imagination doesn't even extend to the idea that a linked list would ever be copied. "Like whaddya mean? The list nodes are embedded in the task control blocks ... you'd have to duplicate the actual processes themselves. It makes no sense." Idiomatic C code uses structs for linked lists, not void * pointers to binary cells consisting of two void * pointers, one of which is actually an int value. I also don't understand why the example function is casting (void **) r when r already has that type. Here is something more reasonable, still with the shallow-copy issue of the pointers-to-integer, and no handling of a null out of malloc. The code is very easy to follow: struct cons { int *car; struct cell *cdr; }; struct cons *listcopy(struct cons *list) { if (list == 0) { return list; } else { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = listcopy(list->cdr); return ncell; } } If the lists can be long, the stack growth can be a problem; this isn't tail recursive. You want something iterative. One possibility is a two pass version: struct cons *listcopy(struct cons *list) { struct cons *copy = 0; struct cons *out = 0; struct cons *cdr; /* walk list, allocating new nodes, pushing * them onto copy stack */ for (; list; list = list->cdr) { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = copy; copy = ncell; } /* Reverse copy stack in place by popping * all nodes and pushing them onto the out * stack. */ for (; copy; copy = cdr) { cdr = copy->cdr; copy->cdr = out; out = copy; } return out; } Here we can separately verify whether the copy stack is correctly produced, and then correctly reversed into out. The average seasoned C pro will probably jump to this sort of solution, but not use any cons/car/cdr terminology he or she never heard of: struct cons *listcopy(struct cons *list) { struct cons *copy = 0; struct cons **pcdr = © for (; list; list = list->cdr) { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = 0; *pcdr = ncell; pcdr = &ncell->cdr; } return copy; } Using a dummy node on the stack to serve as the list parent, we can notationally eliminate the ** pointer: struct cons *listcopy(struct cons *list) { struct cons dummy = { 0 }, *tail = &dummy; for (; list; list = list->cdr) { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = 0; tail->cdr = ncell; tail = ncell; } return dummy.cdr; }
protoman3000 5y ago
This is all exciting and relevant progress, but the technique does not seem to converge towards a real solution in the long run. We developed higher-level languages like C to specify and generate machine code easier and with less errors. Then it turned out with the higher level language it's easy to make mistakes, too, so let's put another layer of specification language on top to avoid that (e.g. let's do Java). Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. The gist is that computation is not an easy task and we can't avoid the halting problem, but still it is very good to have tools available that make negotiating through bug space easier.
- YeGoblynQueenne 5y ago
  >> Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. That is a risk: if the specification is the entire program written in the specification language, then the same opportunities to make mistakes present themselves when writing the specification, as when writing the program by hand. In this case though the specification language has the advantage of being purely declarative: it's only a statement of pre- and post-conditions without any assumptions about implementation. Such a specification leaves little room for mistakes.
  - amw-zero 5y ago
    Are you aware that a huge percentage of accepted math proofs have errors in them? https://lamport.azurewebsites.net/tla/proof-statistics.html https://lamport.azurewebsites.net/tla/proof-statistics.html. The worm at the core of all formal verification is that we mistakenly believe that a result is absolutely correct because formal logic was employed. Logic can be subtly wrong, even though the argument appears correct. The very act of using logic does not imply actual correctness. This is not a dismissal of the field - just a warning. There are many mistakes that can still be made when formally specifying and verifying. To believe otherwise is pure hubris.
    - 5y ago
YeGoblynQueenne 5y ago
That's very nice but what I always want to see in program synthesis work is a proof of soundness and completeness: does the synthesiser provabl produce only correct programs; and can it produce every correct program? The abstract of the (POPL) paper claims that "the derived programs are ... correct by construction" but what about the transformations to the specification, particularly the post-conditions? That's a bit scary. When and how can post-conditions change?
amw-zero 5y ago
I can't comment on whether or not this will definitely be the future of programming, though I do think it's interesting. The more interesting thing to me is just the idea of separation logic. The functional programming community has this idea that functional programming is the only sound programming model from a logical perspective, because it is very historically rooted in math and logic. Turing machines, by contrast, are much more 'made-up' constructions - they have weird, non-mathematical sounding components like heads and tapes, etc. But, for whatever reason, we can produce extremely fast and small processors that pretty closely resemble Turing machines, and C-style imperative, memory-based code flows naturally from that. And, with separation logic, it can also be firmly rooted in math and logic. That was always my feeling with the functional programming zealots, like they were just ignoring other possible universes. The lambda calculus is one formally sound model of computation, sure, but surely it's not the only one.
thesuperbigfrog 5y ago
The problem with generated code is that it is rarely easy to understand or maintain. Suppose you need to add new features or fix a bug, to do so you will need all of the original specifications and code generation tools. Will those tools work on other platforms? Do they support all of the low level needs of C? For example, do they support bit-level layout for structs or inline assembly? I believe that Rust will make more inroads to replace C in many domains. This will eliminate many of C's known issues that Certified Program Synthesis seeks to address. If you need formal verification or proofs, SPARK https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) is a mature and effective tool with a proven track record. It lets developers write code that is easy to understand and maintain compared to generated code and can formally prove the correctness of programs.
- gravypod 5y ago
  There's nothing wrong with generated code if it's never manually modified. Think of binaries: we never manually edit them but they are essentially "generated". More modern build systems automate this process of hiding the intermediate steps. One great example of this is the way Thrift and gRPC. You never edit the stubs or server code. You just implement an interface.
  - thesuperbigfrog 5y ago
    >> There's nothing wrong with generated code if it's never manually modified. Agreed. The issue is that I have never encountered code that did not need to be changed later. I have encountered generated code for which the code generation system was no longer available and it was a tremendous pain to understand and modify.
    - gravypod 5y ago
      The reason this is a pain is the projects doing that were already starting from a broken position. The code gen should be entirely managed by the build system. You should never need to modify or look at the generated code. If you need to change the generation output you should modify the "compiler" (tool doing the generating) or the input source you are using to generate. Examples: If you want to add an int32 into a protobuf you modify the .proto file with your message. If you want to change `int32` to `int32_t` instead of `int` to make the code generator more multi-arch friendly you'd change the protoc plugin for your language. "I have never encountered code that did not need to be changed" is the wrong mindset to have here. You're thinking of the generated code as source code instead of an internal build step (same thing as Clang or GCC's IR). Also if you're in a situation where "code generation system was no longer available" then your build would never succeed. This should be like saying "gcc was no longer available". It shouldn't be possible and in reality the generated code shouldn't even be checked into the source tree.
api 5y ago
Or you could, you know, use Rust, Go, C#, Java, or some other modern language. C does need to die, but until fairly recently there were not many viable replacements. D isn't bad but isn't "better enough."
- eyelovewe 5y ago
  Java and C# are not capable of programming hardware, in the sense that C and C++ are. There’s nothing “nonmodern” about C or C++ and LLVM was written in such a language that compiles to literal processor instructions. The JVM and dot net runtimes were also written in a lower level language with semantics for memory access via pointers. Despite all the hullabaloo about dangers and footguns, embedded dev, HALs, device drivers, OS schedulers and sundry all are written in C or C++. I’m not even bringing up garbage collection but it’s also a whole big dealbreaker for any low level systems programming. One cannot use malloc inside of boot code or inside of a low latency system call, etc It turns out that Rust has gained some attention and is capable of operating in this space. The inertia of Linux kernel code needing to inter link and being largely in C is one reason why you don’t see random bits of Rust in Linux, but this is not to preclude designing low level systems in Rust.
- mbrodersen 5y ago
  You can’t write high performance code in Java/C#. That’s why the JVM is not written in Java.
  - api 5y ago
    You can in Rust.
mikewarot 5y ago
As you state the problem, this is the wrong solution. All programs have bugs, all compilers have bugs. Bits randomly flip in memory, disk, etc. Stop blaming the wrong things. You ran a program, you gave it all your resources, it got confused, and ran amok. It's YOUR fault. You shouldn't have given it all your resources. You should have only given it access to the minimum set of resources resources required to do the job. Now, generating provable correct code does have its merits, the article should have started with those.
- mbrodersen 5y ago
  Nope. CompCert (a C compiler) has zero bugs. It is formally proven correct down to assembler level.
  - mikewarot 5y ago
    I just cringe at the thought of making that bold of a claim on anything computer related, let alone something as complex as a compiler. So, as long as the specifications, and CPU documentation are correct, it will work as intended, a high percentage of the time. (Random bit flips, disk errors, etc. are still a thing)
    - mbrodersen 5y ago
      I highly recommend learning more about what formal software verification actually is and what it guarantees and what it doesn’t.
sdevonoes 5y ago
I don't get it. The "spatial predicated" spec given in the post is just code, at another level, but just code. You just move the complexity one level up. Sure for some scenarios writing the spec is way easier than writing plain code; but for other scenarios the spec will be as complex as the problem requires it... and so we are again with the same problem "how to write correct specs (or code)". We already tried this in the past: machine code -> assembly -> C -> Haskell -> ...

84 points by tluyben2 5y ago

Looks great. One question though (and this isn't criticism of the research, but just about the presentation/intended audience): why would anyone who's been so 'stubborn' (as they say) so far about sticking with C finally have a change of heart because of this? They clearly prefer to write C themselves, otherwise they'd have already moved on, right? It's not like having a C++-to-C or Rust-to-C compiler would've changed the game for them.

tluyben2 5y ago
(not one of researchers but I submitted this because I like the research) I have not tried Rust for a while so this might have changed, but in the tiny embedded devices I work in, where your 'free' memory is for instance 24kb and the speed of the MCU is a few mhz, there really is only C/asm. You need to mess around with every single byte to make it fit and fast enough. There are surprisingly many of these MCU's around everywhere around us. And you (usually) cannot update their firmware remotely (or at all actually), so it's important it doesn't have massive bugs.
- dataflow 5y ago
  People say this all the time, and maybe it's just my naivete, but I just don't understand why at least something like C++ is not an option in embedded spaces. Sure you might need to avoid operator new() and exceptions or whatever, but you still have so much more power than in plain C even with half the language removed, and avoid so many of the C pitfalls just by that. I know people kept telling me you "need" C for a kernel... and I just ignored them and wrote drivers and even a basic from-scratch kernel in C++, and they all worked just fine, and with so much less pain than C. And honestly, if C++ somehow (I don't understand how, but let's say somehow) has too much overhead... why would another language compiled to C be any better? It just doesn't make sense to me.
  - Animats 5y ago
    You can use C++ on even an Arduino. In fact, the Arduino development development is full C++. You just have to stick to the non-Clib features.
  - tluyben2 5y ago
    C++ is no issue but, to make very small binaries packed with the features we need, you need a lot of fiddling and the end it does not look like c++. Not to mention that most embedded devs (at least in Asian, Africa and eu embedded corps which make deployments of millions of mcu's, not home arduino users: there might be more of those) work mostly with C. I think most are waiting to skip a revolution to something like Rust but that does not fit yet. So this solution gives at least some handles to add verification. That said, there are more of these projects. I think there is an F* project too. > why would another language compiled to C be any better? It just doesn't make sense to me. It seems that the formalization in the article allows for very low level operation which you would use in C while not writing C. As said, sure you can do that in C++ but then you gain little or nothing. I have not tried this, only posted it because I would like for something robust like it to exist. Now we use Coq (or more recent idris) to write things and hand translate them to mcu asm/c.
- pjmlp 5y ago
  Not really, there are options available for those that care to look around. https://www.mikroe.com/mikropascal https://www.mikroe.com/mikropascal https://www.mikroe.com/mikrobasic https://www.mikroe.com/mikrobasic Mikroe is just one possible vendor, there are others.
  - tluyben2 5y ago
    Sure, you can: Forth works too. But C is the standard (in my world anyway) so it would be c++ or rust. C++ already is used but Rust I have not seen yet.
    - pjmlp 5y ago
      Sure but you worded it as universal condition, hence my remark. If anything, just to raise awareness for others. Even C++ alone is already an improvement, provided it isn't just C compiled with a C++ compiler, e.g. AUTOSAR.
      - tluyben2 5y ago
        Yep, I agree but we never could make that fit. When it fit, it was just compiled with a c++ compiler pretty much. But I have not met an experienced c++ embedded dev in my industries: all are c/asm because it is always the cheapest (and thus most underpowered) we can get away with given the consumption demands.
- kaba0 5y ago
  Messing around with every single byte is a property of low-level languages. There is absolutely nothing C does differently than C++ or Rust. Hell, it may even be slower due to not having proper abstraction powers and programmers thus lazily choose the easier route with eg. linked lists. Also, due to rust’s semantics it can get better optimizations due to no pointer aliasing.
  - tluyben2 5y ago
    I will try it again then. What is your experience with it in very small devices? As I read online still, the binaries would not fit in the mcus we use. Maybe I am missing something there which has changed or I just missed. I would love to see a realistic (not hello world) example on a 32kb mcu. So with significant amount of function points (we do decryption, signing, otp generation, display driver, keyboard, and lot more and people told me and I read online this would not work well with Rust but this is maybe outdated or maybe the code will just look like C? I don't know examples of anything realistic): think that would turn me and more people.
    - kaba0 5y ago
      If binary size is that important, then there is even better options than C: Zig.
      - tluyben2 5y ago
        Well, every 0.01$ counts for these components as orders are in the millions or 10s of millions. Everything that can be cut gets cut. And now lead times count as well as there are shortages and some factories have many waifers of these low spec ones to sell. I tried Zig on Linux and it is nice: any restricted embedded examples? I will try both Rust and zig when I get home to see if it could even work.
- gradschool 5y ago
  Devil's advocate question for a person who likes this research: What formal definition of a "program synthesizer" would exclude C compilers from being program synthesizers? Similarly, what precisely distinguishes C or any other programming language from a "specification" language?

makerofthings 5y ago

That example they use to show how bad C code is and how complicated pointers can be. That’s just bad C, really bad. And how do I know if he removed a line? You could ask the same question about code in any language.

tluyben2 5y ago
The example is called listcopy, so assuming it does that, I don't think there are many modern languages where you could remove a line and have other (experienced) programmers not pick up on that. Unless that line had nothing to do with the actual task, but that's not the case here. Agreed it is bad code though. A good C example and then synthesised code of the same task would have been better imho.
- comex 5y ago
  > The example is called listcopy, so assuming it does that, I don't think there are many modern languages where you could remove a line and have other (experienced) programmers not pick up on that. Thing is, if the hypothesis is that the complexities of pointers make C harder to read than other languages, this example does not prove that, because its use of pointer features is completely gratuitous. Below I attempted to write a saner version of the same C function. I removed the pointer arithmetic and casts in favor of just using a struct, not because I wanted to avoid those features for demonstration purposes, but because that's what any sane C code would do. I also changed it from accepting a pointer-to-pointer, where the pointee is originally the input value and is then replaced with the output value, to just taking the input as an argument and returning the output – again, because that's the simple and obvious choice. As it happens, the resulting code's use of pointers is limited enough that it could be directly transliterated to Java or any other high-level imperative language. Change the `malloc` to a `new`, fix up the syntax, and you're done. Therefore, whatever lack of clarity remains, it can't be due to anything peculiar to C. (I'd say at this point that the code is clear enough that most people would notice if you removed a line, but YMMV. To be fair, my version also shares some flaws with the original such as not checking for allocation failure.) That said, there are plenty of algorithms which are complex or subtle enough that even in a well-written implementation, someone might not notice a line being removed. But that can happen in any language, at least to some extent. struct list { int value; struct list *next; }; struct list * listcopy(struct list *list) { if (list != NULL) { struct list *copied = malloc(sizeof(*list)); copied->value = list->value; copied->next = listcopy(list->next); return copied; } else { return NULL; } }

rustybolt 5y ago

When I first read the snippet, I thought "What a terrible piece of code.". Later on, I read: "In fact, the code written above was actually entirely automatically synthesised by our tool, along with a proof certificate, formally guaranteeing its correctness." So it looks like the code is terrible, and they only give an example for a simple usecase. So I'm not very enthousiastic about using this technique in practice. The rest of the post looks very informative though, although I haven't completely read it yet.

zozbot234 5y ago
> So it looks like the code is terrible, and they only give an example for a simple usecase. Yes, I'm very skeptical about this being "the future of coding!" (quoting the OP). These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. Typically, a developer has to step in and provide the right invariant so that the tool can get unstuck. Proof synthesis has exact the same issue, so generating proof-carrying code is also something that cannot thus far be automated except in very simple cases. Having said that, separation logic can be a valuable low-level tool and has been used to assess the correctness of, e.g. Rust borrow checking, which aims to provide lightweight, composable guarantees that can scale up to encompass larger programs. Even there though, we're nowhere near an actual proof, and soundness issues have in fact cropped up in the past as new features got added.
- YeGoblynQueenne 5y ago
  >> These tools typically get stuck as soon as one needs to deal with non-trivial loops or recursive code, because it's not clear how to "synthesize" the correct loop invariant or inductive hypothesis; in particular, this cannot be done "compositionally" or "step-by-step" as in the simple case OP demonstrates. By "inductive hypothesis" do you mean the inductive case in a recursion? If so, I'm curious, why do you say this? My experience is that the problem with learning recursion is constructing the "base case", particuarly when there is no example of it. Do you have specific examples where the inductive case is hard to find when learning from specifications?

shannongreen 5y ago

As someone who has to write C for their day job, I am a little bit offended by the introduction of this article, but I guess that's the point. The code presented is trash and doesn't follow best practices - using the type system, descriptive variable names, etc. Void pointers for everything, are you serious? Of course it's hard to understand. Revealing that it's the generated code doesn't make me any more comfortable with it. Yes, I get that you shouldn't care what the generated code looks like if you trust your input, but I don't find the predicate any easier to understand. How do I know that's correct? What if I need to debug this generated output?

pjmlp 5y ago
I have seen code written like that by humans, namely offshored projects.
dang 5y ago
I've taken "Goodbye C developers" out of the title above, since it's pretty linkbaity.

fjfaase 5y ago

The code snippet is incorrect. I do not see a check on malloc returning null. In general that would be okay, but in an embedded environment with limited memory, that would be a serious problem. Also, using recursion is bad, because copying a long list will lead to a stack overflow.

omnicognate 5y ago
It's never OK. Machines with lots of memory run out of memory too. To present a piece of research in such trollish terms, accusing "stubborn C developers" of causing security vulnerabilities, and then present an example of code for which "we didn't even have to bother reasoning about how exactly it did its pointer manipulations" that segfaults if it runs out of memory (it dereferences the result of malloc and writes to that location 2 lines down) is beyond hilarious.
- bestouff 5y ago
  On Linux machines malloc()'s returning NULL doesn't mean you're out of memory, it means you're out of address space which is very different.
  - fjfaase 5y ago
    If I understand it correctly, it is even worse, because malloc could return not NULL and still throw an exception when you try to write to the 'allocated' memory. See for example https://linuxembedded.fr/2020/01/overcommit-memory-in-linux https://linuxembedded.fr/2020/01/overcommit-memory-in-linux
  - omnicognate 5y ago
    In a system with virtual memory there are a variety of limits you can hit that will prevent your process allocating more memory and cause malloc to return zero. It's normal to informally lump all these together as "running out of memory" when the distinction doesn't matter, as here. Address space size is one of these limits, not the only one. Hitting it is rare on 64-bit operating systems, common on 32-bit ones.

pjmlp 5y ago

Every tool is welcomed for the scenarios where there is no workaround as to keep writing C code, but for everything else, the best is not to write it to start with. In any case very interesting paper, however I feel such kind of tooling can only be enforced in scenarios where code certification is already taking place, e.g. MISRA and AUTOSAR.

Animats 5y ago

OK, so you write pre and post conditions for a function, and the function gets generated. OK, so now we're programming at the specification level. I've written formal specifications for an operating system. They're harder to write than code for non-trivial programs. Some things are trivial to specify but hard to code. A hash table, for example. It's easy to specify what a hash table does, but that gives no guidance on how to implement one. You might get out something that does a linear search. File systems and databases are similarly not too hard to specify - the specification describes the abstract brute-force approach. They need to get much further along before announcing victory.

vidarh 5y ago
You indirectly get at an important point: A complete specification must include best/worst/anortised performance constraints, and a lot of other details we often leave unstated. And then it gets a lot harder...
- qayxc 5y ago
  A complete specification also must include assumptions about external systems and limits. Here the assumptions are infinite stack (or item count < stack size limit) and a malloc that never fails. Incomplete specs are just as bad as buggy code. I'd even argue that incomplete specs are worse in this scenario, because the "proven correctness" gives a false sense of security.
- amw-zero 5y ago
  Performance is not a part of behavior. Specification is about specifying logical behavior and that's it. I don't know of any specification framework that supports saying anything about performance.
dexen 5y ago
In programming, coding is a tool for discovering the under-specified parts of the specification.
YeGoblynQueenne 5y ago

kazinator 5y ago

> a simple, standard, procedure to copy a linked list: Using the same argument for the input and output, when making a copy, is idiotic, not standard. Well, maybe idiotic is standard, but that's another discussion. Copying linked lists is not a widespread practice in C programs, by the way; if we don't count C programs that are Lisp interpreters. It creates memory handling problems. In this example, the nodes carry data consisting of integer values. These are referenced by pointers. The copy is shallow-copying these pointers, which could be an issue. If the integers are dynamically allocated, who cleans them up? They have to persist as long as either list is still reachable. The average embedded C programmer's imagination doesn't even extend to the idea that a linked list would ever be copied. "Like whaddya mean? The list nodes are embedded in the task control blocks ... you'd have to duplicate the actual processes themselves. It makes no sense." Idiomatic C code uses structs for linked lists, not void * pointers to binary cells consisting of two void * pointers, one of which is actually an int value. I also don't understand why the example function is casting (void **) r when r already has that type. Here is something more reasonable, still with the shallow-copy issue of the pointers-to-integer, and no handling of a null out of malloc. The code is very easy to follow: struct cons { int *car; struct cell *cdr; }; struct cons *listcopy(struct cons *list) { if (list == 0) { return list; } else { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = listcopy(list->cdr); return ncell; } } If the lists can be long, the stack growth can be a problem; this isn't tail recursive. You want something iterative. One possibility is a two pass version: struct cons *listcopy(struct cons *list) { struct cons *copy = 0; struct cons *out = 0; struct cons *cdr; /* walk list, allocating new nodes, pushing * them onto copy stack */ for (; list; list = list->cdr) { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = copy; copy = ncell; } /* Reverse copy stack in place by popping * all nodes and pushing them onto the out * stack. */ for (; copy; copy = cdr) { cdr = copy->cdr; copy->cdr = out; out = copy; } return out; } Here we can separately verify whether the copy stack is correctly produced, and then correctly reversed into out. The average seasoned C pro will probably jump to this sort of solution, but not use any cons/car/cdr terminology he or she never heard of: struct cons *listcopy(struct cons *list) { struct cons *copy = 0; struct cons **pcdr = © for (; list; list = list->cdr) { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = 0; *pcdr = ncell; pcdr = &ncell->cdr; } return copy; } Using a dummy node on the stack to serve as the list parent, we can notationally eliminate the ** pointer: struct cons *listcopy(struct cons *list) { struct cons dummy = { 0 }, *tail = &dummy; for (; list; list = list->cdr) { struct cons *ncell = malloc(sizeof *ncell); ncell->car = list->car; ncell->cdr = 0; tail->cdr = ncell; tail = ncell; } return dummy.cdr; }

protoman3000 5y ago

This is all exciting and relevant progress, but the technique does not seem to converge towards a real solution in the long run. We developed higher-level languages like C to specify and generate machine code easier and with less errors. Then it turned out with the higher level language it's easy to make mistakes, too, so let's put another layer of specification language on top to avoid that (e.g. let's do Java). Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. The gist is that computation is not an easy task and we can't avoid the halting problem, but still it is very good to have tools available that make negotiating through bug space easier.

YeGoblynQueenne 5y ago
>> Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. That is a risk: if the specification is the entire program written in the specification language, then the same opportunities to make mistakes present themselves when writing the specification, as when writing the program by hand. In this case though the specification language has the advantage of being purely declarative: it's only a statement of pre- and post-conditions without any assumptions about implementation. Such a specification leaves little room for mistakes.
- amw-zero 5y ago
  Are you aware that a huge percentage of accepted math proofs have errors in them? https://lamport.azurewebsites.net/tla/proof-statistics.html https://lamport.azurewebsites.net/tla/proof-statistics.html. The worm at the core of all formal verification is that we mistakenly believe that a result is absolutely correct because formal logic was employed. Logic can be subtly wrong, even though the argument appears correct. The very act of using logic does not imply actual correctness. This is not a dismissal of the field - just a warning. There are many mistakes that can still be made when formally specifying and verifying. To believe otherwise is pure hubris.
  - 5y ago

YeGoblynQueenne 5y ago

That's very nice but what I always want to see in program synthesis work is a proof of soundness and completeness: does the synthesiser provabl produce only correct programs; and can it produce every correct program? The abstract of the (POPL) paper claims that "the derived programs are ... correct by construction" but what about the transformations to the specification, particularly the post-conditions? That's a bit scary. When and how can post-conditions change?

amw-zero 5y ago

I can't comment on whether or not this will definitely be the future of programming, though I do think it's interesting. The more interesting thing to me is just the idea of separation logic. The functional programming community has this idea that functional programming is the only sound programming model from a logical perspective, because it is very historically rooted in math and logic. Turing machines, by contrast, are much more 'made-up' constructions - they have weird, non-mathematical sounding components like heads and tapes, etc. But, for whatever reason, we can produce extremely fast and small processors that pretty closely resemble Turing machines, and C-style imperative, memory-based code flows naturally from that. And, with separation logic, it can also be firmly rooted in math and logic. That was always my feeling with the functional programming zealots, like they were just ignoring other possible universes. The lambda calculus is one formally sound model of computation, sure, but surely it's not the only one.

thesuperbigfrog 5y ago

The problem with generated code is that it is rarely easy to understand or maintain. Suppose you need to add new features or fix a bug, to do so you will need all of the original specifications and code generation tools. Will those tools work on other platforms? Do they support all of the low level needs of C? For example, do they support bit-level layout for structs or inline assembly? I believe that Rust will make more inroads to replace C in many domains. This will eliminate many of C's known issues that Certified Program Synthesis seeks to address. If you need formal verification or proofs, SPARK https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) is a mature and effective tool with a proven track record. It lets developers write code that is easy to understand and maintain compared to generated code and can formally prove the correctness of programs.

gravypod 5y ago
There's nothing wrong with generated code if it's never manually modified. Think of binaries: we never manually edit them but they are essentially "generated". More modern build systems automate this process of hiding the intermediate steps. One great example of this is the way Thrift and gRPC. You never edit the stubs or server code. You just implement an interface.
- thesuperbigfrog 5y ago
  >> There's nothing wrong with generated code if it's never manually modified. Agreed. The issue is that I have never encountered code that did not need to be changed later. I have encountered generated code for which the code generation system was no longer available and it was a tremendous pain to understand and modify.
  - gravypod 5y ago
    The reason this is a pain is the projects doing that were already starting from a broken position. The code gen should be entirely managed by the build system. You should never need to modify or look at the generated code. If you need to change the generation output you should modify the "compiler" (tool doing the generating) or the input source you are using to generate. Examples: If you want to add an int32 into a protobuf you modify the .proto file with your message. If you want to change `int32` to `int32_t` instead of `int` to make the code generator more multi-arch friendly you'd change the protoc plugin for your language. "I have never encountered code that did not need to be changed" is the wrong mindset to have here. You're thinking of the generated code as source code instead of an internal build step (same thing as Clang or GCC's IR). Also if you're in a situation where "code generation system was no longer available" then your build would never succeed. This should be like saying "gcc was no longer available". It shouldn't be possible and in reality the generated code shouldn't even be checked into the source tree.

api 5y ago

Or you could, you know, use Rust, Go, C#, Java, or some other modern language. C does need to die, but until fairly recently there were not many viable replacements. D isn't bad but isn't "better enough."

eyelovewe 5y ago
Java and C# are not capable of programming hardware, in the sense that C and C++ are. There’s nothing “nonmodern” about C or C++ and LLVM was written in such a language that compiles to literal processor instructions. The JVM and dot net runtimes were also written in a lower level language with semantics for memory access via pointers. Despite all the hullabaloo about dangers and footguns, embedded dev, HALs, device drivers, OS schedulers and sundry all are written in C or C++. I’m not even bringing up garbage collection but it’s also a whole big dealbreaker for any low level systems programming. One cannot use malloc inside of boot code or inside of a low latency system call, etc It turns out that Rust has gained some attention and is capable of operating in this space. The inertia of Linux kernel code needing to inter link and being largely in C is one reason why you don’t see random bits of Rust in Linux, but this is not to preclude designing low level systems in Rust.
mbrodersen 5y ago
You can’t write high performance code in Java/C#. That’s why the JVM is not written in Java.
- api 5y ago
  You can in Rust.

mikewarot 5y ago

As you state the problem, this is the wrong solution. All programs have bugs, all compilers have bugs. Bits randomly flip in memory, disk, etc. Stop blaming the wrong things. You ran a program, you gave it all your resources, it got confused, and ran amok. It's YOUR fault. You shouldn't have given it all your resources. You should have only given it access to the minimum set of resources resources required to do the job. Now, generating provable correct code does have its merits, the article should have started with those.

mbrodersen 5y ago
Nope. CompCert (a C compiler) has zero bugs. It is formally proven correct down to assembler level.
- mikewarot 5y ago
  I just cringe at the thought of making that bold of a claim on anything computer related, let alone something as complex as a compiler. So, as long as the specifications, and CPU documentation are correct, it will work as intended, a high percentage of the time. (Random bit flips, disk errors, etc. are still a thing)
  - mbrodersen 5y ago
    I highly recommend learning more about what formal software verification actually is and what it guarantees and what it doesn’t.

sdevonoes 5y ago

I don't get it. The "spatial predicated" spec given in the post is just code, at another level, but just code. You just move the complexity one level up. Sure for some scenarios writing the spec is way easier than writing plain code; but for other scenarios the spec will be as complex as the problem requires it... and so we are again with the same problem "how to write correct specs (or code)". We already tried this in the past: machine code -> assembly -> C -> Haskell -> ...