Writing from MLambda
On verification before construction, neuro-symbolic AI, actors, and languages in which the common corruptions cannot be written.
-
The LLM never answers. Only proofs do.
Why the only way to let language models build software you can trust is to put a symbolic layer in charge of what they say.
-
The intelligence LLMs are missing
A language model predicts the next token over a manifold. Finding a bug is a different act — logic and mathematics — and MLambda's model checker, analysers and derived tests are built to supply it.
-
The future I see
Code is about to be cheap. Quality is not. Why I spent years on actors, logic and proofs while the industry bet on scale — and why I am still betting against it.
-
The formula is the model
A typed algebra language that compiles into your project, a symbolic runtime that differentiates and integrates as pure functions, and the statistics to put stochastic work beside it — built to be carried to other languages.
-
The code era is over
Software engineering information belongs in the requirements, the domain language and the architecture model — not in the code. Genesis is the foundry that makes the code a consequence.
-
System 2 for machines
Language models are System 1 — fast, fluent, intuitive, and unable to check themselves. The next level of AI is a System 2 that reasons in logic. MLambda builds that engine.
-
Refusal is a result
One small system going through Turing, and what it looks like when software declines to be built wrong.
-
Prolog in C#, declaratively
Shin is a rule language whose programs become C# at build time — forward chaining, tabled backward chaining, term rewriting, four modal logics, and a proof tree for every answer.
-
Nowhere to occur
What a pure language does to a bug — and why MLambda built one that still reaches the machine.
-
No locks
What happens when you build a distributed database entirely out of actors — and specify its consistency model before you trust it.
-
Efficiency by construction
Where the speed in an actor-native stack actually comes from — and which of those gains are structural rather than tuned.
-
Context that has been proved
Retrieval hands a language model passages that look relevant. MLambda hands it an ontology that has been admitted, a verdict that says how much it knows, and statistics it can reason about modally.
-
A computer algebra system for engineers, in C#
Symbolic differentiation, integration, expansion and root-finding as a .NET library — and a typed rule language that compiles new algebra into it.