https://github.com/yatima-inc/yatima Skip to content Sign up * Why GitHub? Features - + Mobile - + Actions - + Codespaces - + Packages - + Security - + Code review - + Project management - + Integrations - + GitHub Sponsors - + Customer stories- * Team * Enterprise * Explore + Explore GitHub - Learn and contribute + Topics - + Collections - + Trending - + Learning Lab - + Open source guides - Connect with others + The ReadME Project - + Events - + Community forum - + GitHub Education - + GitHub Stars program - * Marketplace * Pricing Plans - + Compare plans - + Contact Sales - + Education - [ ] [search-key] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this organization All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} yatima-inc / yatima * Notifications * Star 97 * Fork 3 A programming language for the decentralized web MIT License 97 stars 3 forks Star Notifications * Code * Issues 8 * Pull requests 4 * Actions * Projects 3 * Wiki * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Wiki * Security * Insights main Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags 26 branches 0 tags Code Clone HTTPS GitHub CLI [https://github.com/y] Use Git or checkout with SVN using the web URL. [gh repo clone yatima] Work fast with our official CLI. Learn more. * Open with GitHub Desktop * Download ZIP Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Go back Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Go back Launching Xcode If nothing happens, download Xcode and try again. Go back Launching Visual Studio Code Your codespace will open once ready. There was a problem preparing your codespace, please try again. Latest commit @gabriel-barrett gabriel-barrett Merge pull request #67 from yatima-inc/gb/ check-lty-fix ... ecbfdd3 Jun 7, 2021 Merge pull request #67 from yatima-inc/gb/check-lty-fix LTY check fixed ecbfdd3 Git stats * 270 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time .github/workflows Fix signing key Jan 18, 2021 cli Readd wasm target (#53) Jun 3, 2021 core LTY check fixed Jun 7, 2021 nix Readd wasm target (#53) Jun 3, 2021 utils Readd wasm target (#53) Jun 3, 2021 web Readd wasm target (#53) Jun 3, 2021 .envrc WIP Add support for hashspace access in WASM web Mar 31, 2021 .gitignore Readd wasm target (#53) Jun 3, 2021 Cargo.lock Readd wasm target (#53) Jun 3, 2021 Cargo.toml Readd wasm target (#53) Jun 3, 2021 LICENSE update license to MIT Jan 12, 2021 README.md Fix comments host web version from rocket Apr 8, 2021 default.nix Add nix.dev setup and shellHook Jan 18, 2021 flake.lock Readd wasm target (#53) Jun 3, 2021 flake.nix Add grin as a nix dependency May 7, 2021 rustfmt.toml add rustfmt (#56) Jun 1, 2021 shell.nix go-ipfs compatibility achieved Apr 21, 2021 yatima.nix Readd wasm target (#53) Jun 3, 2021 View code Yatima: A programming language for the decentralized web Build Instructions: With Nix: Compiling to WASM With cargo Usage Instructions: Motivation README.md Yatima: A programming language for the decentralized web built with nix --------------------------------------------------------------------- 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 doing matches 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. On an implementation level: * Yatima's core reduction machine is based on the l-DAG technique described in Bottom-up b-reduction. * Yatima's approach to inductive datatypes is based on Self Types for Dependently Typed Lambda Encodings. * Yatima's quantitative types are based on Syntax and Semantics of Quantitative Type Theory. * Many aspects of the language, particularly its libraries and type-equality algorithm, are adapted from the authors' previous work on The Formality proof language. * The hashexpr content-addressing schema is an adaptation of IPFS' Multiformats and IPLD to align with Rivest's Canonical S-exprssions rather than JSON. Come chat with us on Matrix: #yatima:matrix.org Build Instructions: Clone this repository and cd into it: git clone git@github.com:yatima-inc/yatima.git ... cd yatima With Nix: Set up dev environment assuming nix, lorri and direnv are installed. direnv allow This should load correct versions of dependencies into your shell. To build yatima using naersk: nix-build yatima.nix To install the yatima binary into your environment: nix-env -i -f yatima.nix To run the test-suite and CI: nix-build default.nix Niv fixes upgrading dependencies for development. Compiling to WASM wasm-pack build --target web Host the experimental web version with: yatima hashspace server With cargo To build yatima: cargo build To run the test-suite: cargo test --all To install the yatima binary: cargo install --path . Usage Instructions: Parse a .ya file (like from https://github.com/yatima-inc/introit) with: yatima parse Bool.ya Run the main expression in a Yatima package with yatima run HelloWorld.ya Enter the interactive Yatima REPL with yatima repl Motivation We're still in the early days of the Computing Revolution. The first general-purpose digital computers were only switched on about 75 years ago. The living memory of your parents and grandparents extends into the past before computers. These machines are shockingly new, and as a species we really have no idea what they're for yet. We're in the middle of an epochal transformation whose nearest precedent is the invention of writing. There are a lot of prognostications of what that means for our future; lots of different, and sometimes contradictory, visions of how computing is going to continue to shape our minds, our bodies, and our relationships with one another. Yatima, as a project, has an opinionated view of that future. We think computing should belong to individual users rather than corporations or states. A programming language is an empowering medium of individual expression, where the user encounters, and extends their mind through, a computing machine. We believe "Programmer" shouldn't be a job description, anymore than "scribe" is a job description in a world with near-universal literacy. Computing belongs to everyone, and computer programming should therefore be maximally accesible to everyone. Currently, it's not: There are about 5 billion internet users worldwide, but only an estimated 25 million software developers. That's a "Programming Literacy rate" of less than 1%. Furthermore, that population is not demographically representative. It skews heavily toward men, the Global North, and those from privileged socioeconomic or ethnic backgrounds. This is a disgrace. It is if we live in some absurd dystopia where only people with green eyes play music. A new programming language isn't going to be some panacea that solves that problem on its own, but there are some ways in a programming language can help: 1. Build a simple, but powerful programming language. Yatima's core logic is under 500 lines of code, but is incredibly expressive in its type system, runtime and syntax. We want to reduce the language's conceptual overhead, without hindering the language learner's future growth and power. 2. Make explicit in the language the connection between computing and mathematics. These two seemingly separate fields are actually, in essence, the same: All proofs are programs, all programs are proofs. A student doing math homework is programming, even if they don't conceptualize at such. Many people dislike math due to the tedium of manual computation and the unclear relevance of the results. And many people dislike programming because the concrete mechanics often seem arbitrary and frustrating. These are are complementary complaints. Math is more fun when you have a computer to take care of the detail-work. And computing is much easier when you have a clear notion of the theory of what you're doing. 3. Be portable in execution. Run locally, in the browser, on mobile, in a distributed process. People shouldn't have to worry about the details of where they want to do something, only what they want to do. 4. Be portable in semantics. Pure semantics and reproducible builds let people focus on the actual content of their programs rather than the scut-work of configuring infrastructure. 5. Integrate with decentralized technologies to remove, as much as possible, social barriers and frictions. Having centralized services like most modern package managers raises the question "Who controls the package server?" The famous leftpad incident is commonly presented as a build system issue (which it absolutely is), but less frequently discussed is that what precipitated the incident was how the npm administrators transfered ownership of a package from an individual developer without their consent to a large company. 6. Have a clear code of conduct to combat the endemic toxicity of contemporary programming culture. Some might find this controverisial, but it shouldn't be. Computing is a social and cultural project as much as it is a technical one. Cultures which perpetuate cycles of trauma are less successful in the long run than ones which do not. The future we want to build is one where billions of people use, understand and love their mathematical computing machines, as natural extensions of themselves. A future where users have autonomy and privacy over their own systems and their own data. A future where reliable, type-checked, formally-verified software is the norm, so you can rely on software engineering with the same quotidian confidence you have for civil engineering whenever you drive your car over a bridge. About A programming language for the decentralized web Resources Readme License MIT License Releases No releases published Packages 0 No packages published Contributors 6 * @johnchandlerburnham * @gabriel-barrett * @Anderssorby * @samuelburnham * @brightly-salty * @atanmarko Languages * Rust 97.9% * Nix 1.9% * Other 0.2% * (c) 2021 GitHub, Inc. * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.