Data structure implementation tips/pointers

[Alex MárquezPérezMuñízDíazPurasThaureauxFagúndo (Alex)]

Hey all,

I’ve almost finished laying down the foundations of a non-VonNeuman, non-Harvard ternary abstract computer architecture.  I’ve been planning to use Idris2 as the source for this model; however, there are a few key data structures that I would have to build up first, and I’d like to gather some feedback as to places to read/study what’ll help, code to leverage, etc.

I’m leveraging Idris2 because QTT can allow me to prove runtime-irrelevancy/erasure, 1st-class linear types make state machines a breeze, I’ll need to prove key properties such as non-interference, and it compiles down to Racket so I can hook it up directly to a Redex model and broader pipeline/toolchain.

The first, main thing I’ll need is a means of representing a 26-connected 3D Store. Out of what exists in the Idris2 standard distribution, the best option I’ve seen is to nest 3 levels of Vectors; something which would make things very messy.  I’ll be needing to move within that 3D space in a 26-directional digital space, so proving properties and relationships from one such move twixt two very-differently-looking 3D coordinates via a linear hierarchy of 1D sequences… also seems very messy. Keeping a 1D indexable sequence of triples of coordinates also sounds little better.

I’ll also need to be implementing PDAs and NWAs, wherein the latter I’ll also wish to take advantage of the full Boolean Algebra they’re complete over.

In general I don’t plan to go a Hoare-Logic-esque route, but I won’t rule it out entirely. There’ll definitely be a couple other Separation Logics in use, though. (God-willing I won’t have to go to the lengths of porting/mimicking Agda’s Cubical.)

I realize this is a tall, broad, and deep mountain range, nevermind that I haven’t (yet) publicized anything on the topic. The code will be strong copyleft, so I’m happy to incorporate most open source libraries.

I welcome any feedback and critique, and I’ll answer all I can.

Thanks!

Alex M