It's a bit unfortunate that [1] doesn't seem to mention Fleece[2], since Fleece is an already existing, solid format with very similar properties (JSON-compatible data format, uses offsets for sharing, allows for cheap updates, and uses binary search on arrays to achieve O(ln n) lookups in large tables or arrays, etc.)
It's not "obviously" typed. Values in python have (runtime) types, sure. But contrast that with a statically typed language in which expressions (and functions) have types. Expressions in python do not have types at all (at least before annotations were added).
Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...
I'm not sure you can call the type rules for CiC "intuitive for programmers". They're quite powerful and go further than "type of argument matches expected type".
Compared to CoC, first order logic is a model of simplicity, and I think it's reasonable to argue that adding the inductive types to get to CiC is as complex as adding a handful of axioms to Fol to obtain ZFC. And don't forget to pick a flavor of universe polymorphism or cumulativity to make it usable. That's not exactly simple.
I think there's a good case for CiC or HoTT being nice and usable for mathematicians. I don't think they're simple or more appealing to programmers. A kernel for metamath is the simplest, and it has more independent implementations than any other system.
Odin and Zig solve almost all the memory safety aspects, except for use after free. Having bound checks, union types, etc. is good and a real improvement over C, but I think that use after free is a memory unsafety issue. It's the one that's harder to tackle because it's more dynamic ("temporal memory safety"?).
Maybe it's because real engineering has higher stakes than a crud app. Condos can kill, bridges can kill, Javascript forms or video game engines generally can't. If they could we'd witness a lot more deaths, despite your confidence.
What if your domain problem (say, compilers, symbolic algorithms) doesn't have a clear notion of ownership because everything is a shared DAG that may survive for arbitrarily long? Not every problem has clear ownership imho (and tools in C or C++ in these domains resort to their own refcount/custom GC implementation anyway).