The future of programming with certified program synthesis

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.

Also, using recursion is bad, because copying a long list will lead to a stack overflow.

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) 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.

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.

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.

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.

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.

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?

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;
    }
  }

  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;
 }

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;
  }

  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;
  }

We already tried this in the past:

machine code -> assembly -> C -> Haskell -> ...

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?

C does need to die, but until fairly recently there were not many viable replacements. D isn't bad but isn't "better enough."

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.