Writing from MLambda
On verification before construction, neuro-symbolic AI, actors, and languages in which the common corruptions cannot be written.
-
The room and the tower
A language model is Searle's Chinese Room with a better calculator. Believing that scale will turn it into a mind is building the Tower of Babel again — and the mind, like God, may be the one object that cannot be studied from outside.
-
The mind is not in the shadow
If the world we see is a three-dimensional projection of a reality with more dimensions, then consciousness belongs to the part we do not see. That is why no scan has found it, why we only ever meet it as intention, and why a machine built entirely inside the shadow will not contain it.
-
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.
-
Malkhut and the world of ideas
Kabbalah describes the ascent of consciousness as a departure from Malkhut, the manifest world, towards worlds above it. Read as a map of projection, it dissolves Descartes' problem. We are not a mind attached to a body. We are a mind, seen in three dimensions.
-
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.