Viewing profile — nathanrf

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

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 : (…

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

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

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

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

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…

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…

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…

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…

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

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

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

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

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; // …

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…

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 …