Idris2-proved progressive type safety for WebAssembly linear memory (regions are tables, loads are queries) — and the verified convergence ABI that independent WasmGC languages agree on.
-
Updated
Nov 11, 2026 - Idris
Idris2-proved progressive type safety for WebAssembly linear memory (regions are tables, loads are queries) — and the verified convergence ABI that independent WasmGC languages agree on.
A four-pane neurosymbolic development environment (eNSAID) designed as a cognitive-relief layer for human-machine co-orbit. Built on AffineScript (TEA architecture) and Ephapax (Gossamer webview), with friction monitoring (Vexometer), neural output gating (Anti-Crash); planned TypeLL (type) and ECHIDNA (proof) verification for the symbolic layer.
Fixed-layout PDF and application-form filling for boxes, baselines, and per-character cells designed for hand spacing; Firefox UI with a Rust-WASM core.
Resource-safe, effect-typed programs in syntax you already know. A checked affine core with familiar Faces — JavaScript-, Python-, functional-, and pseudocode-shaped surfaces — compiling to typed WebAssembly.
Pseudocode-syntax AffineScript — first-language for CS pedagogy that compiles and runs
JavaScript/TypeScript-syntax AffineScript — affine resource guarantees + typed-wasm output for JS/TS-shaped code
Python-syntax AffineScript — write Python-style code, get affine resource guarantees and typed WASM
Type-theoretic verification kernel for formally verified database queries, providing dependent, linear, session, quantitative, effect, and modal type coverage. Idris 2 formal specs, Rust verification kernel, Zig FFI bridge, JSON-RPC protocol. The "LLVM of type safety" for query validation.
Semantic lattice builder for git repositories using AffineScript
Pick the algebra, get the discipline...and still have totality
Retro driving game written in AffineScript. Test Drive III: The Passion-inspired — perspective road rendering + centripetal-force steering. Prototype.
Curated AffineScript learning, reference, examples and community resources, with honest maturity labels.
Parallel corpus crawler and alignment index across 1,500+ languages, for preserving languages and cultures and connecting people through them. Starts from Bible translations for their unmatched coverage; designed to carry provenance and terms of use with every text. For research, localisation and accessibility.
Local-first bowtie risk and opportunity workbench for sociotechnical safety, human factors and organisational learning: browser UI with IndexedDB storage and an AffineScript/WebAssembly policy kernel.
Reusable AffineScript libraries (design stage): a KYAML (Kubernetes YAML) lexer/AST/parser draft, with jq-style query DSLs, Kubernetes lint rules, data structures and FFI bindings planned. Intended core of kcq.
systemet is a stratified type theory. The name is system + ET, where ET stands for Equality Theory — because the one primitive relation the whole system keeps at the bottom is equality, and everything else is layered above it as discipline rather than added as new relations.
Holy f$£%ing s%£$, get the f$£% out of the way! Use picture-in-picture and be able to do things without another monitor.
To associate your repository with the affinescript topic, visit your repo's landing page and select "manage topics."