akiarie

9 ms·

31.
by akiarie 3y ago
> The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation? This is a pivotal question and our answer to it exposes one of our basic assump
32.
by akiarie 3y ago
> I don't think you're under any obligation, I just think that not discussing prior art is a bad look. See [0] where our reliance on Dijkstra is transparent. > I don't see anything new about the application of these wel
33.
by akiarie 3y ago
It cannot in general deduce the abstract. Doing so would require solving the halting problem.
34.
by akiarie 3y ago
"Simpler" is the word that we care about. Although Rust is an advance on C in many significant ways, what it loses is the simplicity. One of our goals is to offer three same advances (and more) but without compromising on simplici
35.
by akiarie 3y ago
Interesting points. Because it's easy to do the type checking at compile time for function prototypes (though we haven't implemented it yet) we haven't felt under pressure to use the `func(void)` notation, which has always fe
36.
by akiarie 3y ago
Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on. We aren't claiming to have invented these techniques. It should be obvious that Xr0 involves ver
37.
by akiarie 3y ago
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.
38.
by akiarie 3y ago
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
39.
by akiarie 3y ago
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 t
40.
by akiarie 3y ago
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
41.
by akiarie 3y ago
A lot of truth to this. (Speaking as one of the creators of Xr0).
42.
by akiarie 3y ago
> 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.
43.
by akiarie 3y ago
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 preproce
44.
by akiarie 3y ago
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 unsatisf
45.
by akiarie 3y ago
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 languag
46.
by akiarie 3y ago
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
47.
by akiarie 3y ago
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
48.
by akiarie 3y ago
> 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 rul
49.
by akiarie 3y ago
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.
50.
by akiarie 3y ago
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 (progra
51.
by akiarie 3y ago
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.
52.
by akiarie 3y ago
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 multithread
53.
Xr0 Makes C Safer than Rust(xr0.dev)
49 points by akiarie 3y ago|41 comments
54.
Dennis Ritchie's criticisms of an early draft of C89(port70.net)
1 points by akiarie 3y ago|0 comments
55.
On the teaching of programming, i.e. on the teaching of thinking (EWD473)(raboof.github.io)
2 points by akiarie 3y ago|0 comments
56.
by akiarie 3y ago
We'll think this through. (Honestly, we've been focused on C89 and I heard about C23 attributes today.)
57.
by akiarie 3y ago
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 gett
58.
by akiarie 3y ago
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.
59.
by akiarie 3y ago
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 sa
60.
by akiarie 3y ago
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.

More ›