In one sense, the Truth Mines were just another indexscape. Hundreds of thousands of specialized selections of the library’s contents were accessible in similar ways–and Yatima had climbed the Evolutionary Tree, hopscotched the Periodic Table, walked the avenue-like Timelines for the histories of fleshers, gleisners, and citizens. Half a megatau before, ve’d swum through the Eukaryotic Cell; every protein, every nucleotide, even carbohydrate drifting through the cytoplasm had broadcast gestalt tags with references to everything the library had to say about the molecule in question.
In the Truth Mines, though, the tags weren’t just references; they included complete statements of the particular definitions, axioms, or theorems the objects represented. The Mines were self-contained: every mathematical result that fleshers and their descendants had ever proven was on display in its entirety. The library’s exegesis was helpful-but the truths themselves were all here.
Diaspora, Greg Egan
Yatima is a pure functional programming language implemented in Rust with the following features:
- Content-Addressing powers reproducible builds, and peer-to-peer package management. A Yatima content-address represents an immutable program and all its dependencies. That means if someones shares an address with you, you can perfectly replicate their computation (and in principle even their computing environment!). Since the program is immutable, the way it runs the first time is the way it runs everytime.
- First-class types. This lets you the programmer to tell the compiler what you intend to do in your program. Then, like a helpful robot assistant, the compiler will check to make sure that what you’re actually doingmatches those expressed intentions. Type-driven programming lets the compiler act as your “correctness exocortex”, i.e. a cognitive augmentation that helps you catch your mistakes.
- Linear, affine and erased types give you fine-grained control over resource usage during execution. Substructural types allow you to get the memory safety benefits of using a high-level language, while also allowing you to work “close to the metal” when you want to.
- Type-safe dependent metaprogramming lets Yatima have the flexibility and extensibility of a dynamically-typed language, without sacrificing the safety of static-typing.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.