GADTs let you do similar things in the simplest cases, they just don't work as well for complex constraints. Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on…
In the style of the linked post, you'd probably define a generic type (well, one of two generic types): type ExactlyStatic : (0 t: Type) -> (0 v: t) -> Type type ExactlyRuntime : (0 t: Type) -> (v: t) -> Type Then you…
The two commands affect the same account balance, so they don't commute, so these commands conflict. Every EPaxos worker is required to be able to determine whether any two commands are conflicting, in this case it…
This is the (pre-print) paper produced from that project - i.e. it is a self-contained, complete description of the work completed so that it can be reviewed, and then cited. The underlying result has not changed, but…
It is as simple as: the person who contributed the proofs/implementations chose Rocq. I did some small proofs in Dafny for a few of the simpler deciders (most of which didn't end up being used). At the time, I found…
Here's a high level overview for a programmer audience (I'm listed as an author but my contributions were fairly minor): [See specifics of the pipeline in Table 3 of the linked paper] * There are 181 million ish…
I'm not involved in this rewrite, but I made some minor contributions a few years ago. TSC doesn't use many union types, it's mostly OOP-ish down-casting or chains of if-statements. One reason for this is I think…
The quoted paragraph is correct as written. E.g. if f: ∀A, B. A -> B -> A Then we have poly type π = "∀A, B. A -> B -> A". The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge…
The paper defines them as programs in a process calculus (which is fairly standard as far as theory for protocols is involved): Definition 1 (Asserted protocols) Asserted protocols, or just protocols for short, are…
Feral != Native. There are no honeybee species native to North America; all honeybees, including the feral ones, are descended from colonies imported from Europe (e.g. the "Western honeybee" apis mellifera). There are a…
It is a good thing that cppfront lets you do that, then! Cppfront generates #line pragmas which tell the generated .cpp file which source lines to "blame" for each piece of generated code. This isn't something new and…
Unfortunately, C++ uses ++ and -- for iterators, many of which cannot reasonably implement += or -=. This distinction is baked into the type system to tell whether or not an iterator supports efficient "multiple…
The distortion comes from trying to map R^2 onto the surface of the mesh, since they have different curvature, so they only "match" near the origin. But the random-walk algorithm doesn't actually need to happen in R^2;…
`const`-as-comment is specifically limited to pointers and references - `const` on objects definitely does change semantics (it is always UB to attempt to modify a `const` object). Another good example is string…
That is saying exactly the same thing that I said; the qualification of the pointer is irrelevant; you get UB when modifying a const object. In the code snippets above, int x; // not a const object, so can be freely…
In C and C++, `const` on pointers/references is basically just a comment to programmers - it is part of the type, but doesn't "mean" anything to the abstract machine; the rules don't treat const / regular…
It is unsound to transmute `&'a T` into `&'static T`, but it is not UB - as long as all of the subsequent uses of the transmuted reference obey the "real" lifetime of the original reference: fn example<'a>(r: &'a mut…
GADTs let you do similar things in the simplest cases, they just don't work as well for complex constraints. Like, append: Vector n t -> Vector m t -> Vector (n+m) t. With GADTs you need to manually lift (+) to work on…
In the style of the linked post, you'd probably define a generic type (well, one of two generic types): type ExactlyStatic : (0 t: Type) -> (0 v: t) -> Type type ExactlyRuntime : (0 t: Type) -> (v: t) -> Type Then you…
The two commands affect the same account balance, so they don't commute, so these commands conflict. Every EPaxos worker is required to be able to determine whether any two commands are conflicting, in this case it…
This is the (pre-print) paper produced from that project - i.e. it is a self-contained, complete description of the work completed so that it can be reviewed, and then cited. The underlying result has not changed, but…
It is as simple as: the person who contributed the proofs/implementations chose Rocq. I did some small proofs in Dafny for a few of the simpler deciders (most of which didn't end up being used). At the time, I found…
Here's a high level overview for a programmer audience (I'm listed as an author but my contributions were fairly minor): [See specifics of the pipeline in Table 3 of the linked paper] * There are 181 million ish…
I'm not involved in this rewrite, but I made some minor contributions a few years ago. TSC doesn't use many union types, it's mostly OOP-ish down-casting or chains of if-statements. One reason for this is I think…
The quoted paragraph is correct as written. E.g. if f: ∀A, B. A -> B -> A Then we have poly type π = "∀A, B. A -> B -> A". The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge…
The paper defines them as programs in a process calculus (which is fairly standard as far as theory for protocols is involved): Definition 1 (Asserted protocols) Asserted protocols, or just protocols for short, are…
Feral != Native. There are no honeybee species native to North America; all honeybees, including the feral ones, are descended from colonies imported from Europe (e.g. the "Western honeybee" apis mellifera). There are a…
It is a good thing that cppfront lets you do that, then! Cppfront generates #line pragmas which tell the generated .cpp file which source lines to "blame" for each piece of generated code. This isn't something new and…
Unfortunately, C++ uses ++ and -- for iterators, many of which cannot reasonably implement += or -=. This distinction is baked into the type system to tell whether or not an iterator supports efficient "multiple…
The distortion comes from trying to map R^2 onto the surface of the mesh, since they have different curvature, so they only "match" near the origin. But the random-walk algorithm doesn't actually need to happen in R^2;…
`const`-as-comment is specifically limited to pointers and references - `const` on objects definitely does change semantics (it is always UB to attempt to modify a `const` object). Another good example is string…
That is saying exactly the same thing that I said; the qualification of the pointer is irrelevant; you get UB when modifying a const object. In the code snippets above, int x; // not a const object, so can be freely…
In C and C++, `const` on pointers/references is basically just a comment to programmers - it is part of the type, but doesn't "mean" anything to the abstract machine; the rules don't treat const / regular…
It is unsound to transmute `&'a T` into `&'static T`, but it is not UB - as long as all of the subsequent uses of the transmuted reference obey the "real" lifetime of the original reference: fn example<'a>(r: &'a mut…