ERIS is intended to fit into this use-case. A simple spec with a simple privacy feature and 1KiB block size for things like trees of metadata (RDF).
(I was paid to do some work on ERIS so I have an interest in promoting it.)
1 Like
We have the univalent foundations of mathematics and a current implementation that makes these notions computable, the cubical type theory extension in Agda.
But they haven’t figured how to compile the univalent axiom into an executable yet, the one that makes one type compatible with the other.
https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
Another new very promising effort is the narya theorem prover, it makes a much stronger argument about the relation of the two types and it is definitional, at least this is what I understand.
An example:
You have two types of R^2, the Cartesian XY coordinates and the circular? Coordinates RΘ.
You can program in the type you want that is easier at the time, and then transfer all your programs to the other type.
(Proofs from one type are transfered to the other…)
1 Like
Hello, the part about using data objects in 3D space in social context reminds me of some cooler VRChat worlds:
VRChat World: “Experience” by Nootau
Linux in a Pixel Shader - A RISC-V Emulator for VRChat
YouTube - Revisiting ShaderFes 2019
What about https://www.unison-lang.org/? It works with a canonical form of the AST, with names just being a local convenience for developers, and different people can have different ones, for the same code.
1 Like
Thanks - ERIS looks pretty good! The convergence key solves one major privacy issue, while still making it possible to use a null key if we really just want open public data archives with deduplication.
That’s definitely a sensible approach.
I guess I keep thinking about two main use cases at the same time: sort of North and South poles to steer by. In my mind a system for the future must be able to handle both of these cases:
One, Uxn-scale (or perhaps just Dusk-scale) ultra-minimalist systems. We should have a language core that can be coded from scratch on a 64k machine with 16-bit words. Needs to be simple and clear to understand and implement. This is to be a teaching tool, and to solve the “trusting trust” bootstrap problem. The core compiler must be absolutely tiny and able to be coded from scratch.
Two, Web-scale personal data clouds and desktops. The system – preferably the same language core as the 64k version just on bigger/faster hardware – needs to be able to handle at least UTF8 text, PDFs, JPGs and video files fetched from remote servers and cached on a local multi-terabyte SSD, or several. It needs to be able to handle file sizes larger than 2GB, and never download anything more than once. If necessary (and with enough people/resources), it must be able to store Wikipedia, the Internet Archive, and Github - ie, a civilization reboot kit - but just smallish individual chunks of that, like a person or family’s entire Web presence, email archive, photos, videos, and personal documents would be fine. It must be fast enough to act as a realtime desktop OS over as minimal and portable an underlying hardware abstraction as we can get. It should use as much RAM and as many CPU cores as are available to implement a private compute/storage cloud, and it needs to have clear boundaries (multiple of them) between what storage, transmission and compute zones are local and trusted vs which are remote and untrusted. All data must be able to be exported and imported in large chunks, probably encrypted zipfile, with enough redundancy to be stored in multiple locations and quickly imported into different systems decades later or rapidly under disaster conditions (say, a wildfire or war or fascist regime that both trashes your city and compromises its data centers and all you can save is the nightly backup on USB drive or encrypted online file of your personal home data cloud), with very little shared context.
These two seem to me to be the bare minimum edge cases. Tiny trusted core, easily built, but which can also save and load its state in big easily portable chunks, and can scale to 64-bit sized systems of filesystems.
1 Like
That’s one perspective, and it’s a very valid one. Programs (or even tiny computable expressions like just one function call or variable reference) should never be able to break out of their secure context and either read or write memory or variables or call functions that they do not have a reference for. And when even tiny cheap home machines come with terabytes of persistent storage, exposing that whole address space as mutable storage to any function you evaluate (as Dusk does) feels like dangerous madness. Fire-walking in an explosives factory while drunk level madness.
However: there’s another perspective, and that’s the perspective of data.
If someone hands me a copy of Moby Dick, I do not want it to be possible for them to tell me “you MAY NOT EVER quote individual words from this book; that’s dangerous and forbidden. The text must remain hidden to you for your safety. You MAY ONLY interact with this book by performing a magic ritual which summons one of the book’s characters, and you may then talk only to that character, and only ever in terms of abstract Themes from the book, as defined by the author. These Themes must be structured as defined by the author, and no theme is allowed which the author has not previously permitted. Also, the book will destructively rewrite itself as your conversation proceeds, and you might never be able to reset the state of the book, because you are forbidden from ever learning that state.”
That may sound silly, yet it’s the extreme form of the Object Oriented “the object controls all its interactions” philosophy. It doesn’t seem quite right to me, but it’s hard to pinpoint where “don’t let the user accidentally trash their entire life’s dataset with one click” ends and “I am App Developer the All Powerful and I own your soul now” begins.
A book may contain high-level themes, but the system book API must allow me to interact with it as a low-level sequence of raw characters, and the book must not get a choice about this. Otherwise it’s not a book, it’s live theatre.
We have too much live theatre in our software today, and too few books.
The app-less version of Moby Dick is “my personal dataset of all the emails I’ve written, all the files I’ve stored, all my appointments and social media posts”.
Obviously, I don’t want every random email attachment to be able to read my address book or get root on my hard drive: that’s the Microsoft Office OLE pit of pain, which we would do well to study to learn how not to do that.
But as the author/owner of all that data, I do want the right to drill into any part of it, extract one email or one post or one date from an appointment, and give that data item to any other app or function call of my choice. I don’t want my calendar view saying “hey no you can’t share that” when the data is right there; the calendar view/app has no business forbidding me use rights over my own data.
5 Likes
Brilliant. Exactly right. I’ll probably use the Moby Dick story myself in conversation!
1 Like
I’m implementing for ARM Cortex M4 (Nordic nRF52) and for PC-class (Linux) only. The same code runs on both (well, the ARM chip can’t do Vulkan yet…) So I’m upgrading your 16 bit words anyway. I love “civilization reboot kit” - I’ll be using that as well! I’ll bear in mind the NFRs of your top-end architecture.
1 Like