6 ms·

If 0v can tell what the abstract needs to be, why do we need to write it down? It has to know the abstract to compare against the annotation. Maybe it's so we b

by irq-1 3y ago

If 0v can tell what the abstract needs to be, why do we need to write it down? It has to know the abstract to compare against the annotation. Maybe it's so we better understand the origin of the problem, rather than getting 'free error' at the end of a long chain of functions?

akiarie 3y ago
It cannot in general deduce the abstract. Doing so would require solving the halting problem.
- muldvarp 3y ago
  It also can't in general deduce whether the abstract and the implementation match, as doing so would require solving the equivalence problem (which is undecidable for anything as or more powerful than pushdown automata).
  - akiarie 3y ago
    I'm not very familiar with the equivalence problem, but at least for Xr0 abstracts (what we call the annotations attached to functions & loops) there is an extremely strong structural similarity between the implementation and the annotation. So it's not at all clear that we'll run into this.
    - muldvarp 3y ago
      > there is an extremely strong structural similarity between the implementation and the annotation. If the annotation is basically just a copy of the function body why have any annotation at all? > So it's not at all clear that we'll run into this. It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
      - akiarie 3y ago
        > If the annotation is basically just a copy of the function body why have any annotation at all? This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard). They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly. Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g. #include <stdlib.h> void foo() ~ [ return malloc(1); ] { return malloc(1); } void bar() { void *p = foo(); free(p); } void baz() { bar(); /* completely safe */ } Note that `foo`'s annotation is like a copy of its body, but `bar`'s annotation is very simple, even though it interacts with `foo`, which is only safe if the pointer it returns is handled. So from `baz`'s perspective there are no safety semantics it has to worry about when it interacts with `bar`. The complexity that could lead to safety bugs in `foo` has been completely handled in `bar`. We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0. > It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this. Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.
        muldvarp 3y ago
        > Xr0 annotations seem to be copies of the function bodies, but they aren't actually. You're constantly dodging the question. If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical). > Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0. So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".

by irq-1 3y ago

akiarie 3y ago

It cannot in general deduce the abstract. Doing so would require solving the halting problem.

muldvarp 3y ago
It also can't in general deduce whether the abstract and the implementation match, as doing so would require solving the equivalence problem (which is undecidable for anything as or more powerful than pushdown automata).
- akiarie 3y ago
  I'm not very familiar with the equivalence problem, but at least for Xr0 abstracts (what we call the annotations attached to functions & loops) there is an extremely strong structural similarity between the implementation and the annotation. So it's not at all clear that we'll run into this.
  - muldvarp 3y ago
    > there is an extremely strong structural similarity between the implementation and the annotation. If the annotation is basically just a copy of the function body why have any annotation at all? > So it's not at all clear that we'll run into this. It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
    - akiarie 3y ago
      > If the annotation is basically just a copy of the function body why have any annotation at all? This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard). They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly. Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g. #include <stdlib.h> void foo() ~ [ return malloc(1); ] { return malloc(1); } void bar() { void *p = foo(); free(p); } void baz() { bar(); /* completely safe */ } Note that `foo`'s annotation is like a copy of its body, but `bar`'s annotation is very simple, even though it interacts with `foo`, which is only safe if the pointer it returns is handled. So from `baz`'s perspective there are no safety semantics it has to worry about when it interacts with `bar`. The complexity that could lead to safety bugs in `foo` has been completely handled in `bar`. We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0. > It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this. Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.
      - muldvarp 3y ago
        > Xr0 annotations seem to be copies of the function bodies, but they aren't actually. You're constantly dodging the question. If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical). > Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0. So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".