nathanrf

5 ms·

1.
by nathanrf 11mo ago
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 the types,
2.
by nathanrf 11mo ago
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 could
3.
by nathanrf 11mo ago
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 would be something l
4.
by nathanrf 1y ago
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 the presentation of th
5.
by nathanrf 1y ago
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 Dafny's &
6.
by nathanrf 1y ago
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 essentially differ
7.
by nathanrf 2y ago
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 performance;
8.
by nathanrf 2y ago
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
9.
by nathanrf 2y ago
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 ranged over by S an
10.
by nathanrf 2y ago
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 lot of non
11.
by nathanrf 2y ago
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 fancy f
12.
by nathanrf 2y ago
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 advance" (e.g. a l
13.
by nathanrf 3y ago
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; I thin
14.
by nathanrf 3y ago
`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 literals (except when init
15.
by nathanrf 3y ago
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 modifie
16.
by nathanrf 3y ago
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 refer
17.
by nathanrf 3y ago
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&