Designing Code for Human Reasoning

Formal proofs are powerful, but in real-world software they often become longer than the code—and sometimes more error-prone than what they’re trying to validate. Automated tools help, but they aren’t always available, expressive enough, or feasible to adopt everywhere.

What follows is a practical middle path: semi-formal reasoning about correctness. Not mathematics. Not vibes. Just structured thinking strong enough to convince a devil’s-advocate peer reviewer.

“If you can clearly argue why a small section is correct, you usually understand it well enough to trust it.”

1. The Middle Path: Reason in Small Sections

The trick is to divide code into short sections—often a single line to a block under ~10 lines—and reason about each one. Choose boundaries so that the program state at each end is easy to describe: the relevant variables, the important objects, and what must be true before/after.

• Entry property: what must already be true before this section runs
• Exit property: what will be true after it completes
• Single job: the section should do one describable transformation

When you do this consistently, code becomes easier to review, test, and modify— because correctness arguments stay local instead of bleeding across the system.

2. Kill Hidden Dependencies: Avoid Modifiable Global State

Global mutable state makes reasoning brittle because correctness depends on invisible, distant writes. Your “proof” becomes: “I think no one changed this value”… which is not a proof at all.

Before

public static int DiscountRate;

public decimal CalculatePrice(decimal price)
{
    // Correctness depends on global state: who changed DiscountRate, and when?
    return price - (price * DiscountRate / 100);
}

After

public decimal CalculatePrice(decimal price, int discountRate)
{
    // Correctness depends only on explicit inputs
    return price - (price * discountRate / 100);
}

Reasoning upgrade: you can now state a clean precondition: “discountRate is between 0 and 100.” No guessing. No hidden coupling.

3. Prefer Immutability: Reduce the Number of Possible States

Mutable objects multiply the number of states you must consider. Immutability collapses the state-space and makes invariants stick.

Before

public class Order
{
    public decimal Total { get; set; } // can change anytime
}

After

public class Order
{
    public decimal Total { get; }

    public Order(decimal total)
    {
        Total = total;
    }
}

Reasoning upgrade: downstream logic can treat Total as a stable fact, not a moving target.

4. Collapse Nested Condition Reasoning Into One Truth

Deep nesting forces reviewers to simulate multiple branches. Extract the eligibility rule into one predicate so the “why” is explicit, reusable, and testable.

Before

if (order != null)
{
    if (order.Items.Any())
    {
        if (order.Total > 1000)
        {
            ApplyDiscount(order);
        }
    }
}

After

if (IsEligibleForDiscount(order))
{
    ApplyDiscount(order);
}

static bool IsEligibleForDiscount(Order? order)
{
    return order != null
        && order.Items.Any()
        && order.Total > 1000;
}

Reasoning upgrade: you reason once about eligibility, then treat it as a trusted building block.

5. Keep Functions Short and Single-Purpose

Long methods hide multiple sections inside one blob. Semi-formal reasoning works best when a function has narrow intent and predictable state changes.

Before

public void ProcessOrder()
{
    Validate();
    CalculateTotals();
    ApplyDiscount();
    Save();
    NotifyCustomer();
    Log();
}

After

public void ProcessOrder()
{
    ValidateOrder();
    FinalizePricing();
    PersistOrder();
}

Reasoning upgrade: your review becomes “Is FinalizePricing() correct?” not “Is this whole blob correct?”

6. Limit Parameters: Localize Invariants

Parameter explosions make it unclear which combinations are valid. Grouping related data moves validation and invariants into one place.

Before

void CreateUser(string name, string email, int age, string role, bool active)

After

void CreateUser(UserProfile profile)

Reasoning upgrade: rules like email validity, age range, and role constraints can live inside UserProfile, shrinking reasoning at every call site.

7. Narrow Interfaces: Don’t Pull State Out—Push Behavior In

Getter-driven designs spread reasoning across boundaries. Instead, ask objects to do the work with the state they already own.

Before

// External code must understand internal rules and mutate state safely
if (account.Balance > amount)
{
    account.Balance -= amount;
}

After

// Object owns the invariant and the rules
account.Withdraw(amount);

Developer Wisdom: encapsulation is not “hiding fields.” It’s minimizing what others must know to use your object correctly.

8. Protect Invariants: Prefer Intent Methods Over Setters

Setters invite arbitrary state changes and accidental invariant breaks. Prefer explicit state transitions that enforce rules in one place.

Before

order.Status = OrderStatus.Completed;

After

order.MarkAsCompleted();

Reasoning upgrade: correctness becomes: “Does MarkAsCompleted() enforce the rules?” instead of “Did someone set this too early somewhere?”

Closing Thought

You don’t need formal proofs to write correct software. But you do need code that is structured for reasoning: small sections, explicit dependencies, stable state, and narrow interfaces.

The moment you intend to reason about correctness, you automatically start writing better code. That’s not theory—that’s daily engineering.