Skip to content

hyperpolymath/iseriser

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

12 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

The -iser Ecosystem

License: PMPL-1.0-or-later Palimpsest Covenant 29 repos Idris2 ABI Zig FFI

29 Rust CLI tools that inject superpowers from specialist languages into your existing codebase — without you ever learning those languages.


What is the -iser Pattern?

An -iser is a Rust CLI that bridges the gap between a specialist language (a language with unique strengths in a narrow domain) and the code you already write every day. Each -iser:

  1. Reads a declarative TOML manifest describing what you want.

  2. Validates it against a formally verified Idris2 ABI specification.

  3. Generates wrapper code, bindings, or transformations targeting the specialist language — via a Zig FFI bridge for C-ABI compatibility.

  4. Builds and runs the result, giving you the specialist language’s capabilities without leaving your toolchain.

The pattern lets you tap into GPU kernels (Futhark), formal proofs (Idris2, Dafny, TLA+), data-race freedom (Pony), fault tolerance (OTP), distributed computing (Chapel), and 20+ other domains — all through a consistent init / validate / generate / build / run workflow.

Iseriser is the meta-framework that generates new -iser projects. Given a language description, it scaffolds a complete -iser repo in minutes: manifest parser, codegen engine, Idris2 ABI definitions, Zig FFI bridge, 17 CI/CD workflows, RSR governance files, and documentation.

Architecture: Idris2 ABI + Zig FFI

Every -iser in the family shares a three-layer architecture that guarantees interface correctness through formal verification:

                     +---------------------------+
                     |     Rust CLI (cargo)       |
                     |  init/validate/gen/build   |
                     +------+----------+---------+
                            |          |
               +------------+          +------------+
               |                                    |
               v                                    v
  +------------------------+         +------------------------+
  |     Idris2 ABI Layer   |         |   Zig FFI Layer        |
  |  (formal verification) |         |  (C-ABI bridge)        |
  |                        |         |                        |
  |  Types.idr             |-------->|  build.zig             |
  |    dependent types     |  gen'd  |  src/main.zig          |
  |    prove correctness   |   C     |  test/integration.zig  |
  |  Layout.idr            | headers |                        |
  |    memory layout       |         |  zero-cost C interop   |
  |    platform proofs     |         |  cross-compilation     |
  |  Foreign.idr           |         |  no runtime deps       |
  |    FFI declarations    |         |                        |
  +------------------------+         +------------------------+
               |                                    |
               +----------------+-------------------+
                                |
                                v
                   +------------------------+
                   |   Target Language       |
                   |   (Chapel, Futhark,     |
                   |    Idris2, Pony, ...)   |
                   +------------------------+
Why Idris2 for ABI?

Dependent types prove interface correctness at compile time. Memory layouts are verified. Platform-specific ABIs are selected with compile-time proofs. Backward compatibility is provable. These are type-level guarantees that no other approach can provide.

Why Zig for FFI?

Native C ABI compatibility with zero overhead. Memory-safe by default. Cross-compilation is built in. No runtime dependencies. The ideal bridge between formal specifications and real-world calling conventions.

The -iser Family (29 repos)

Name Description Tests Status

TypedQLiser

Add formal type safety (10 levels, dependent/linear/session types) to any query language

0

scaffold

Chapeliser

General-purpose Chapel acceleration — distribute any workload without learning Chapel

22

scaffold

Verisimiser

Augment any database with VeriSimDB octad capabilities — drift, provenance, temporal

26

scaffold

Julianiser

Auto-wrap Python/R data pipelines into Julia for 100x speedups

25

scaffold

Futharkiser

Compile annotated array operations to GPU kernels via Futhark

42

scaffold

Idrisiser

Generate proven-correct wrappers from interfaces using Idris2 dependent types

6

scaffold

TLAiser

Extract state machines from code and model-check with TLA+/PlusCal

32

scaffold

Dafniser

Generate correct-by-construction code for critical functions using Dafny

28

scaffold

Ponyiser

Wrap concurrent code in Pony reference capabilities for data-race freedom

27

scaffold

OTPiser

Generate OTP supervision trees and fault-tolerance scaffolding

1

scaffold

Halideiser

Compile image/video pipelines to optimised Halide schedules

24

scaffold

Lustreiser

Generate formally verified real-time embedded code via Lustre

36

scaffold

BQNiser

Detect array patterns and rewrite as optimised BQN primitives

0

scaffold

Alloyiser

Extract formal models from API specs and verify with Alloy

25

scaffold

ATSiser

Wrap C codebases in ATS linear types for zero-cost memory safety

32

scaffold

Nimiser

Generate high-performance C libraries via Nim metaprogramming

28

scaffold

A2MLiser

Add cryptographic attestation to any markup or configuration via A2ML

0

scaffold

AffineScriptiser

Wrap code in affine + dependent types targeting WASM via AffineScript

36

scaffold

Anvomidaviser

Convert ISU notation to formal figure skating programs via Anvomidav

36

scaffold

BetLangiser

Add ternary probabilistic modelling to deterministic code via Betlang

36

scaffold

Eclexiaiser

Add energy/carbon/resource-cost awareness to software via Eclexia

23

scaffold

Ephapaxiser

Enforce single-use linear type semantics on resources via Ephapax

17

scaffold

K9iser

Wrap configs into self-validating K9 contracts

19

scaffold

MyLangiser

Generate progressive-disclosure interfaces from complex APIs via My-Lang

20

scaffold

Oblibeniser

Make operations reversible and auditable via Oblibeny

27

scaffold

Phronesiser

Add provably safe ethical constraints to AI agents via Phronesis

31

scaffold

WokeLangiser

Add consent patterns and accessibility to existing code via WokeLang

44

scaffold

SqueakWell

Database recovery through cross-modal constraint propagation — 8 modalities

0

scaffold

Iseriser

This repo — the meta-framework that generates all other -isers

24

scaffold

Total tests across the family: 726

Installation

Every -iser is a standalone Rust binary. Install any of them with:

# Install a specific -iser
cargo install typedqliser
cargo install futharkiser
cargo install chapeliser
# ... or any other -iser name

# Install iseriser (the meta-framework)
cargo install iseriser

Or clone and build from source:

git clone https://github.com/hyperpolymath/<name>.git
cd <name>
cargo build --release

Usage

All -isers share the same five-command interface:

# Initialise a new manifest for your project
<iser> init

# Validate your manifest against the Idris2 ABI spec
<iser> validate

# Generate target language code from your manifest
<iser> generate

# Build the generated output
<iser> build

# Run the result
<iser> run

Using Iseriser to Create a New -iser

# 1. Create a language description
cat > mylanguage.toml <<'TOML'
[language]
name = "MyLang"
type_system = ["dependent", "linear"]
target = "native"
calling_convention = "c"
TOML

# 2. Generate the -iser repo
iseriser generate --from mylanguage.toml --output ./mylangiser

# 3. The result is a complete, functional -iser repo
cd mylangiser
cargo test   # tests pass immediately
cargo run -- init

Generated Repo Structure

When iseriser generates a new -iser, it produces:

<name>/
+-- Cargo.toml                        # Rust CLI project
+-- src/
|   +-- main.rs                       # CLI: init/validate/generate/build/run
|   +-- lib.rs                        # Library API
|   +-- manifest/mod.rs               # TOML manifest parser
|   +-- codegen/mod.rs                # Target-specific code generation
|   +-- abi/mod.rs                    # Rust-side ABI types
|   +-- interface/
|       +-- abi/
|       |   +-- Types.idr             # Idris2 type definitions + proofs
|       |   +-- Layout.idr            # Memory layout verification
|       |   +-- Foreign.idr           # FFI function declarations
|       +-- ffi/
|           +-- build.zig             # Zig build config
|           +-- src/main.zig          # Zig FFI implementation
|           +-- test/integration.zig  # FFI integration tests
+-- .github/workflows/                # 17 CI/CD workflows
+-- .machine_readable/                # RSR governance (STATE, META, ECOSYSTEM)
+-- README.adoc
+-- ROADMAP.adoc
+-- TOPOLOGY.md
+-- LICENSE

The Hub

Browse the full -iser family with interactive search and filtering:

The GitHub Pages hub provides:

  • Searchable catalogue of all 29 -isers

  • Architecture diagrams and domain explanations

  • Quick-start guides for each -iser

  • Links to crates.io, documentation, and source

Status

All 29 -iser repos are scaffolded and functional. The architecture is defined, CLI commands work, manifest parsers are operational, and test suites are in place across the family. Domain-specific code generation logic is the current frontier — each -iser is being deepened with real codegen for its target language.

Contributing

See CONTRIBUTING.adoc for guidelines. All contributions must pass the full CI suite including Hypatia neurosymbolic scanning.

License

SPDX-License-Identifier: PMPL-1.0-or-later

Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)

Licensed under the Palimpsest License.

About

Meta-framework that generates new -iser projects from language descriptions

Topics

Resources

License

Code of conduct

Contributing

Security policy

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors