https://arxiv.org/abs/2603.25414

🔬 Numerical stability, computational correctness, physical consistency; this is what we're building at SpeakEZ Technologies. Verified AI infrastructure that's just the beginning of our journey.

#AI #Sustainability #systemsprogramming #quantum

Decidable By Construction: Design-Time Verification for Trustworthy AI

A prevailing assumption in machine learning is that model correctness must be enforced after the fact. We observe that the properties determining whether an AI model is numerically stable, computationally correct, or consistent with a physical domain do not necessarily demand post hoc enforcement. They can be verified at design time, before training begins, at marginal computational cost, with particular relevance to models deployed in high-leverage decision support and scientifically constrained settings. These properties share a specific algebraic structure: they are expressible as constraints over finitely generated abelian groups $\mathbb{Z}^n$, where inference is decidable in polynomial time and the principal type is unique. A framework built on this observation composes three prior results (arXiv:2603.16437, arXiv:2603.17627, arXiv:2603.18104): a dimensional type system carrying arbitrary annotations as persistent codata through model elaboration; a program hypergraph that infers Clifford algebra grade and derives geometric product sparsity from type signatures alone; and an adaptive domain model architecture preserving both invariants through training via forward-mode coeffect analysis and exact posit accumulation. We believe this composition yields a novel information-theoretic result: Hindley-Milner unification over abelian groups computes the maximum a posteriori hypothesis under a computable restriction of Solomonoff's universal prior, placing the framework's type inference on the same formal ground as universal induction. We compare four contemporary approaches to AI reliability and show that each imposes overhead that can compound across deployments, layers, and inference requests. This framework eliminates that overhead by construction.

arXiv.org

Published today on arXiv: https://arxiv.org/abs/2603.25414

🔬 Numerical stability, computational correctness, physical consistency; this is what we're building at SpeakEZ Technologies. Verified AI infrastructure that's just the beginning of our journey.

#AI #Sustainability #systemsprogramming #quantum

Decidable By Construction: Design-Time Verification for Trustworthy AI

A prevailing assumption in machine learning is that model correctness must be enforced after the fact. We observe that the properties determining whether an AI model is numerically stable, computationally correct, or consistent with a physical domain do not necessarily demand post hoc enforcement. They can be verified at design time, before training begins, at marginal computational cost, with particular relevance to models deployed in high-leverage decision support and scientifically constrained settings. These properties share a specific algebraic structure: they are expressible as constraints over finitely generated abelian groups $\mathbb{Z}^n$, where inference is decidable in polynomial time and the principal type is unique. A framework built on this observation composes three prior results (arXiv:2603.16437, arXiv:2603.17627, arXiv:2603.18104): a dimensional type system carrying arbitrary annotations as persistent codata through model elaboration; a program hypergraph that infers Clifford algebra grade and derives geometric product sparsity from type signatures alone; and an adaptive domain model architecture preserving both invariants through training via forward-mode coeffect analysis and exact posit accumulation. We believe this composition yields a novel information-theoretic result: Hindley-Milner unification over abelian groups computes the maximum a posteriori hypothesis under a computable restriction of Solomonoff's universal prior, placing the framework's type inference on the same formal ground as universal induction. We compare four contemporary approaches to AI reliability and show that each imposes overhead that can compound across deployments, layers, and inference requests. This framework eliminates that overhead by construction.

arXiv.org
Explore the Wild West of post-POSIX IO Interfaces with Anil Madhavapeddy! A lively VMIL'25 talk about new IO abstractions, performance, and systems design - perfect for OS devs, researchers, and curious programmers. Tune in! #VMIL25 #POSIX #IO #SystemsProgramming #OperatingSystems #AnilMadhavapeddy #English #TechTalk
https://crank.recoil.org/videos/watch/323e1d45-3cf6-4554-9d96-db730c3df8a7
[VMIL'25] The Wild West of post-POSIX IO Interfaces

PeerTube

Why Rust for the runtime?

- Portable (runs anywhere)
- Strongly typed
- Predictable under concurrency
- Safe to embed
- Fast enough to sit in the middle

Basically: "I want this to run everywhere and not explode"

#rustlang #systemsprogramming

The Cost of Indirection in Rust

Why 'indirection has a cost' is usually the wrong reason to inline and what actually costs you.

Selective Creativity
Rust 1.94.0 Released with Array Windows and Cargo Improvements

Rust 1.94.0 introduces array_windows for slices, Cargo config inclusion, TOML 1.1 support in Cargo, and stabilized APIs in const contexts.

TechLife
Deep dive into k-CAS: Vesa Karvonen breaks down sweat-free techniques for concurrent, lock-free programming with clear slides and full speaker notes — perfect for systems engineers and PL enthusiasts. Enlightening and practical! #kCAS #Concurrency #LockFree #ParallelComputing #SystemsProgramming #ProgrammingLanguages #VesaKarvonen #Tarides #English
https://watch.ocaml.org/videos/watch/acebc363-12df-4cd6-aec0-e8239ab325e0
k-CAS for sweat-free concurrent programming by Vesa Karvonen

PeerTube

Ruby provides a powerful interface for building native extensions, allowing Ruby code to call C functions directly.

The article walks through:

• the structure of a Ruby C extension
• compiling with extconf.rb
• argument conversion between Ruby and C
• wrapping native structures
• using Rust as an alternative for building extensions

Includes practical code examples for building your first native Ruby binding.

https://rubystacknews.com/2026/03/04/writing-ruby-bindings-for-c-libraries/

#ruby #systemsprogramming #opensource

Writing Ruby Bindings for C Libraries

Writing Ruby Bindings for C Libraries March 4, 2026 Building Native Extensions with C (and Rust) Ruby is known for its productivity and elegant syntax, but sometimes performance-critical tasks requ…

Linking Ruby knowledge from the most remote places in the world.

Design goals:

- Zero friction: header-only, self-compiling C scripts, one-line install
- Safety + liveness: invariants for "never" properties, goals for "eventually" properties
- Multi-path verification: `FROM`/`TO` macros to check reachability from arbitrary states
- Sanitizer support: ASan + UBSan enabled with a single flag

Ideal for protocols, state machines, synchronization logic, anything where exhaustive verification is tractable.

GPLv3. Feedback and contributions welcome.

🔗 codeberg.org/cdsoft/benelos

#C #ModelChecking #FormalMethods #EmbeddedSystems #OpenSource #SystemsProgramming

@cstross @alex_p_roe @timo21

Amusing aside on that score:

I looked at Lynx's vaunted 1991-patented interrupt handling for #LynxOS.

There's prior art for it in the forms of KMOS, an operating system used for teaching purposes by Milan Milenković (who published a book on operating systems in 1987 describing kernel-task-based interrupt handling), and indeed in #Minix too.

#OperatingSystems #KMOS #MessagePassing #SystemsProgramming #RTOS