ggleason

Write it in a theorem prover! No really!

It's really incredible. We decided to see if we could write a Tokio-like library in Lean and were able to do it in a week with performance similar to Node 22. There is really no reason not to use a theorem prover now instead of a functional programming language, and soon it will be better than most languages. All that will remain that it can't do are the jobs of low level languages like C++ [for now].

If you write it in a theorem prover you can have the LLM write proofs about the code quite easily. Lean is easily good enough to compete with javascript, so now I think it makes sense to switch to Lean.

How to use supervised learned classifiers without a training set by using LLMs.

It would be extremely handy to have a document store / graph database which had row polymorphism. I started writing a prototype, but unfortunately never got there. I wonder if any such things already exist?

Those are all interesting ideas.

For the index structure itself you can use succinct dynamic data structures to reduce the size. The bulk loading approach is particularly amenable to use of succinct data structures as the node-vectors in a HNSW are montonic they can use an Elias-Fano encoding. The neighborhoods can use log-arrays.

Creating a multi-index also seems possible, where you use the triangle-inequality to prune the candidate vectors. This will probably require storing the distances for neighbor distances in the bottom layer, in order to be time-efficient for query and would thereby be slightly bigger. I haven't tried it yet but I intend to.

There is also the possibility of using random projection for dimensionality reduction. I also haven't tried this yet either but will give it a go soon. We haven't folded the parallel hnsw into our open source VectorLink yet, but we'll be doing it in the near future - we wanted a little bit of stability of approach first.

TerminusDB founder here. TerminusDB is now at the absolute outer edge of compact data representation. Neo4j is literally 10 times more space for the same data meaning that you'll need 10 times as much memory for a big graph. Succinct datatypes will have their day yet.

TerminusDB represents the data using succinct data structures which reduces the required memory substantially over many other representations. Each branch needs to be capable of being loaded into memory completely - but individual revisions are loaded separately.

Diffs can be constructed between two objects, or you can get sets of diffs of objects between commits automatically. You can manually construct diffs and use them to patch branches.

We don't have a conversion tool from SQL database tables, but it's something on my list.

Yeah, it's really unfortunate that these amazing advances in datalog don't make it into general purpose languages.