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…
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…
`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…
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…
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…
`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…
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…