akiarie

Yes, the code example you've given is exactly in the direction we're thinking. (Edit: thought it can't be verified yet.)

We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states.

The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read.

I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed.

[0]: https://xr0.dev/learn#initialisation-of-memory-and-the-clump

This is another good find. We haven't yet implemented the `!=` operator (or most of the binary operators).

Incidentally, you will notice that Xr0 rejects the program as is, which is correct (because of the double free). It can, however, accept code like the following:

  void
  foo(int a, int b)
  {
          int *p;
          p = malloc(1);
          if (a) {
                  if (!b) {
                          free(p);
                  }
          }
          if (b) {
                  free(p);
          }
          if (!a) {
                  if (!b) {
                          free(p);
                  }
          }
  }

I say "can" because we only have this working on a development branch [0], and there are still some issues we're resolving on this, hopefully by next week.

[0]: https://github.com/xr0-org/xr0/tree/fix/nested-branching

This is another good spot. Xr0's logical/arithmetic analysis is currently limited because we've been more focused on getting the structures of the language working as a whole. So you'll get more of these asserts if you try using `&&`, ternaries, and so on.

We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43

Good spot. We hadn't enabled `else` last week when we posted, but we've just fixed this [0].

[0] https://github.com/xr0-org/xr0/releases/tag/v0.15.0

A lot of truth to this. (Speaking as one of the creators of Xr0).

> Already from the meat of the article, it seems that this solution is setting you up for using a complex language to specify the interface, which immediately begs the question of how you can be sure the interface is correctly specified.

This is insightful. That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it.

The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program. In this way what we're doing is an application of the "trust the programmer" design philosophy; trust him, not only to know what he's doing, but to be able to express it (in the interface specification).

> Sure, in a three-line function, it's kind of obvious (if you know to be aware of this possibility!), but in a function where the pointer and the use are separated by hundreds of lines of code, it's easy to miss that there is a requirement that the hash table not be resized between the two calls. With Rust, the fact that &mut for V means that I can't touch the hash table until I'm finished with V makes it a compiler error.

It can seem as though the example we provide is contrived (because of course it is), but it is not mere contrivance. The point we stress the most is not that the bug is obvious if there are only three lines, but that the presence or absence of a bug is impossible to see even with a single function call whose interface is informal. So what is remarkable is not that we can write three lines of code that have or do not have an obvious error, but that by the mere fact of the interfaces being informal, a three-lined function can be impossible to analyse by itself.

> The ability to mutate an object necessarily implies the ability to mutate the state of an object to break guarantees. While there are definitely patterns where multiple mutable references to the same object can be safe, it is not inherently safe, and proving safety is far more challenging because you can't as easily rely on pre/postconditions for lemmas.

This doesn't answer the question. "it is not inherently safe" does not mean "it is inherently unsafe", it only means "it may be unsafe". So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting.

It's one more step in the build process. Maybe one day we'll imitate Zig and let C compilers be called via Xr0 though.

It also buys as the possibility of beauty. Shoehorning the annotations we're introducing into the preprocessor leads to constructions that aren't nice.

The answer is simple: C isn't going anywhere. Some programmers are satisfied with Rust, and let them enjoy themselves, for as we said, Rust is a great advance for systems programming. But many C programmers, in particular, are unsatisfied with its complexity, as are we, so we're building Xr0 for them (and us).

I like that, "The Mother of Modern Programming Languages". Perhaps it is better to call C the Latin of programming.

> How anyone can think pointer arithmetic is elegant is beyond me. Especially when the title mentions a language with algebraic data types and higher order functions. Or even just RAII.

I have nothing against algebraic data types. They're great. With respect to elegance, I will refer to nothing more than this (from K&R):

  /* strcmp: return <0 if s<t, 0 if s==t, >0 if s>t */
  int strcmp(char *s, char *t)
  {
          for ( ; *s == *t; s++, t++)
                  if (*s == '\0')
                          return 0;
          return *s - *t;
  }

I challenge you to provide a more elegant function with the same specification.

The reason for the new annotation syntax is the annotations are much richer in their details than merely stating when an object is freed by a function. They can express subtle preconditions, such as the expectation that a pointer refer to a region that is heap-allocated, or be a valid lvalue or rvalue, and so on, and also capture more general side effects.

As per the issue of backward-compatibility, Xr0 strips the annotations with a simple command: `0v -s`, producing C source that works with C compilers.

Can you give an example of the kind of data-dependent behaviour you have in mind? We haven't implemented unions yet, but I see no reason why the approach we describe in the article cannot propagate the tagging info in such a struct.

As we explain in the article, Xr0's focus on formalising interfaces allows the verification of each function to be carried out independently. Thus we do reference counting only within individual functions.

I'm not sure I fully understand the CPython example. What I can say is that the annotations allow us to capture the semantics such as whether a function destroys a value, stores its value in a global or returned value, or has no net effect on the state of its caller.

> Without knowing the body of `bar` it's not possible to determine whether `foo` is sound.

This is literally the point we're making in the article. Note that what protects you from violating type safety is not the ownership rules, but the ability to propagate these rules by annotating `bar`. So we're proposing a direct focus on this propagation.

The only limitation to the allocation patterns Xr0 imposes is that there can be no leaks. Everything else is possible.

Yes, Xr0 is young. It took Rust nine years to reach v1.0.0. Xr0 may need slightly over the nine months its had.

Fair enough, I can see how it would seem that way.

The comparison is not meant antagonistically, but almost as tongue-in-cheek.

In making the comparison we're acknowledging that Rust is the touchstone for safety in today's (programming) world. Our praise for Rust in the article shows this.

We said it isn't inherently unsafe. That's not the same thing as calling it safe.

But yes, thread safety is down the road for us, when we get to C11.

You aren't missing anything. It's a good point.

We're beginning with what is central in C and then moving outward. C, as designed by Ritchie, and for the first 40 years of its existence had no official support for multithreading, so this can hardly be called central.

If we add support for multithreading it'll be after finishing with C89 and C99.

We'll think this through. (Honestly, we've been focused on C89 and I heard about C23 attributes today.)

Appreciate the thinking and tinkering. Xr0 has a long way ahead of it before we have a fully-consistent, reliable syntax and set of axioms. For one thing, we delayed implementing the dereference operator `*p` because we were focused on getting our basic model to work with loops (which led us to focus on the array-indexing syntax, e.g. `p[0]`). The below works, but I note that quite a few meaningless or incorrect permutations of the abstract work (and shouldn't).

    #include <stdlib.h>
    
    foo(void **pp) [ .alloc pp[0]; ] {
        void *q;

        q = malloc(4);
        pp[0] = q;
    }

This is a really important question for us. I view it as an issue of tradeoffs.

The advantage of putting the annotations in comments is C compilers can compile the code right away, which may make it easier for existing projects to adopt it.

The disadvantage is that the annotations become second-class citizens, and will never feel native. Placing them in comments also means that they cannot have their own comments unless we introduce another comment sequence for the annotation environment. Again, it means that we can't use the preprocessor, so conditional compilation is impossible.

So basically, we're trading some compatibility for nicer, native-like source. For us, "beauty is the first test", and we believe that there's no way for the source to be beautiful if we put the annotations in comments.

It's most similar to Frama-C/ACSL in terms of the annotative approach.

What's most distinctive about Xr0 is it's built to be reliant on the programmer to structure the code in a way that is amenable to verification of safety. Another unique thing is that the annotation language is C-like and should be easy to pick up for programmers.

The code will compile if the annotations are stripped, and we'll have a command to do this soon.

Good thinking, but it's a bit early for real use — we'll be focused for the next couple of months on getting it self-hosting.

We're looking at this. Some very fascinating stuff. Somewhere at the beginning of "The Calculi of Lambda Conversion" Church talks about the fact that quantification can be reduced to lambdas. I have not read to the end of the paper (still learning these things step by step) and as we have struggled to understand how we should represent quantification, one of the things that became clear is the analogy between functions and quantifiers on the ground that both bind variables, so on the surface what you're talking about has the ring of truth.

> How does i2 compare with other languages used in verification?

I have to plead a measure of ignorance here as the context for my response, though we are working to understand the existing languages.

Perhaps what distinguishes i2 from the existing languages is we're treating this as an engineering rather than a science problem. We aren't trying to build up from the ideal logical system (which is maybe what Coq, Agda, Lean etc. do) but rather, viewing things pragmatically, trying to build a language that requires the least amount of investment for the average practicing mathematician to learn and begin using.

The sense I get (again appealing to ignorance) when I look at most of Coq-style options is that one has to learn type theory and/or constructivism before starting. In this way maybe we're closer to HOL and Isabelle.

Another angle is we're coming from a programming background, and view C as the model for what we're trying to achieve. C somehow captured all the essential capabilities of a Von Neumann machine at the right level of abstraction, and with a very "orthonormal" feature set, such that nearly every major system in the world is written in it or in a language based upon it. Our goal (which may greatly exceed our capacities) is to design something that does the same for maths.

> How are you planning to monetize i2forge?

We aren't sure about this at all. We're just convinced that we have unique insights into this problem and want to work on it full time, so we will be working towards monetising. One idea we've been playing around with is building tools for teachers, or for independent learners.

I think the challenge is it isn't completely obvious to me that starting with 0 is pedagogically correct, though it is so logically. `y >= x + y` is different from `y != x + y`; the former says that addition (of natural numbers) is monotonically increasing, the latter that there is no identity element. Is it possible that admitting an identity element is confusing for beginners? Or is this just a consequence of my own educational conditioning?

(For the record I think all the arguments Dijkstra gives for 0-indexing are correct. I just lack the mathematical intuition to see why the special case above appears to be one in which admission of 0 as complicates things.)

You raise two fine points.

> Natural numbers should start with 0 [0].

I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up going with 1 is we were imitating the structure of the proofs in Landau's "Foundations", and he uses 1 as his first number.

An interesting takeaway was the following. The way he structures his theorems and proofs, he makes use of his assumption that 0 is not a natural number. For example, Theorem 7 in the book is "y != x + y (for all natural numbers x, y)". So I found that sticking to my roots as a programmer (and admirer of Dijkstra) and insisting on zero-indexing led to more complicated theorem statements (e.g. "y != x + y for all natural numbers x, y > 0"). I'm not sure whether this is something structural about how the properties of natural numbers, integers, etc. relate; or whether it's an artefact of Landau's approach.

> Suspiciously, the following lines in the proof can be entirely removed while still verifying:

Suspicion warranted! The first (or zeroth) of these is a bug we hadn't fixed yet (see [1]). Our implementation is rather rough around the edges, but I've put a small fix for this—try again and tell me what you think.

The line "term 1 nat" interestingly isn't used in the theorem we've written, so it's more a mistake on our part for including it in the sample code. Good spot! See the language page [2] for an example where it is used.

As an aside, have you noticed that our proof style is based on what we call "Dijkstra-chaining"? Any thoughts on this? [3]

[0] https://paste.sr.ht/~akiarie/d7a2ae368faae4ba9a8bc13eeefcf18....

[1] https://todo.sr.ht/~lbnz/i2/1

[2] https://i2lang.org/#uses1

[3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E...

Ken Thompson's famous paper on implementing regular expressions is surprisingly simple and yet extremely sophisticated at the same time. The "heart" of the method he proposed was the use of a stack in order to compile the expression to code that parses it, which in this case was IBM 7094 object code.

I find this idea beautiful, and wanted a chance to play around with it for myself, as well as demonstrate to anyone interested the way the algorithm works. Since the aim is demonstration rather than a concrete (or usable) implementation, it makes sense to compile to a high-level language, which is why I have started by targeting Go.

All suggestions are welcome!