Frankly speaking ...

A Reader Pushes Back Why Lean? argued that formal methods are the industry's answer to a world where testing can no longer keep up with the cost of failure. A reader, commenting on that post , pointed out something the post had left out entirely: sometimes bugs survive not because testing failed to catch them, but because nobody was ever going to fix them. That comment, and the conversation it started, turned into more than a reply. It was the second half of the argument. The Bugs We Choose Not to Fix The reader's point was blunt and specific: a company they had just left refused to fix known bugs because the market and investors wanted to see year-on-year growth, and growth comes from shipping new features, not from fixing what already exists. Bugs get "fixed" only when a client trips over one in production. In effect, the user base becomes an informal, unpaid QA layer — crowdsourced testing whether they like it or not. This is a different failure mode from ...

The Real Issue Is Trust Modern society runs on software that is increasingly essential and increasingly fragile. The problem is not simply that code has bugs. The deeper issue is that we have built a digital civilisation on systems whose correctness is assumed rather than demonstrated. The examples are familiar, and they are getting more costly. In 2025, a routine firewall upgrade caused the Optus emergency calling outage : ordinary calls were automatically rerouted to another network without incident, but Triple Zero calls were silently left undelivered for hours. The fault was narrow, yet it landed precisely on the one function that mattered most, raising serious questions about how deeply society depends on systems we assume are safe and reliable. In 2026, the Telstra outage brought widespread disruption across a continent, showing how a single infrastructure failure can cascade through communications, commerce, and daily life. In a world where a single logic error can disabl...

It is a comfortable belief: AI is just a mirror. Critics often dismiss large AI systems, especially large language models, as statistical parrots that reflect our words, images, and ideas without any deeper agency. They argue that such systems cannot come up with new ideas. I think that is wrong. The question is not whether AI has consciousness or human-style understanding. The question is whether it can see associations and links that humans often miss. Human civilisation also advances through copying and recombination. We build on what came before. AI does something related, though in a different manner. It notices connections across vast bodies of data and turns those relationships into outputs that can feel surprising to us. In this essay I will look at several examples — a Go match, a mathematical proof, a rocket engine, a strange portrait, and a drug candidate — where I think AI has done something novel and interesting. Move 37: A Strategy That Broke Human Intuition In Mar...

Introduction: The Informational Universe We typically perceive our world through the lens of tangible matter and flowing energy. We see a landscape of atoms, forces, and heat. However, modern science is beginning to realise that these physical properties might merely be the surface of a deeper architecture. At its most fundamental level, the universe appears to be composed of “bits” of information. Consider the extraordinary feat of a single microscopic cell: how does it “know” how to construct a complex human being? The answer lies not just in chemistry but in the sophisticated processing of data. By shifting our perspective to information theory, we can begin to decode the underlying software of existence and see ourselves as nodes within a vast, self-optimising system. This article follows that idea from first principles to wider systems. It moves from Shannon’s formal definition of information, through biology and thermodynamics, then into active theoretical debates in physics...

Why This Debate Matters Contemporary physics faces a quiet but profound crisis. Our picture of the universe rests on two extraordinary frameworks that do not fit neatly together: General Relativity (GR), which describes spacetime as a smooth continuum curved by mass, and Quantum Mechanics (QM), which describes reality as discrete particles governed by chance. That tension sits alongside another stubborn cosmic puzzle: if the second law of thermodynamics dictates that the universe must become increasingly disordered over time, how can an expanding cosmos give rise to complex, ordered structures like galaxies, stars, planets, and life? Standard cosmology often attributes cosmic acceleration to a static cosmological constant or an undetected form of dynamical dark energy. Gravity from Entropy (GfE), developed by mathematician Ginestra Bianconi , offers a fresh perspective. Rather than adding missing particles or modifying GR arbitrarily, GfE treats gravity as an emergent, thermo...

Using Lean 4 for Mathematics Proofs In the previous post, I explored Lean 4 as a functional programming language. If you already know functional languages like Haskell, you will recognise a lot of familiar ideas. Where Lean starts to feel different is in its annotations and, especially, in its use of tactics with dependent types. To make that concrete, I will walk through a small mathematical proof in Lean 4. The goal is to show an irrationality result. The classic classroom example is that  2 – √  is irrational, but that proof needs extra machinery. Here, I will use a simpler example that only needs basic arithmetic. I will start with the maths proof, then translate the same idea into Lean 4. I like this proof because it is compact. It is the classic “one side must be even, the other must be odd” contradiction. Mathematics: Prove that  log 2 ( 3 )  is irrational I start by assuming  log 2 ( 3 )  is rational. That means there exist positive integers...