The Effect of Functional Programming in Software Verification at Scale

engineering8736
Dec 6
4 min read

Updated: Dec 7

How FP principles helped us build reliable systems, prevent regressions, and ship safely every day.

By Vasilis Nicolaou, Software Engineering Consultant @ Vaslabs. Based on material from talks and supporting notes.

In 1968, at one of the earliest Software Engineering conferences in Garmisch, Germany, the industry’s pioneers were already wrestling with the same question we face today: How do we build software we can trust?

Alan Perlis, Edsger Dijkstra, and others debated the reliability of systems that were rapidly becoming essential to society. Their discussions remain strikingly relevant: testing large systems is hard, correctness is elusive, and reliability is non-negotiable.

Fast-forward to now—an era where software eats not just the world but entire industries—and the challenge remains. At Vaslabs, we’ve spent years refining a practical answer, shaped heavily by functional programming principles applied to real systems at scale.

This article summarises that approach.

Why Functional Programming Matters for Verification

Functional programming (FP) provides more than elegant abstractions—it offers tools to make software easier to test, easier to reason about, and ultimately more reliable.

At the heart of FP lies a simple but transformative idea:

Pure functions always produce the same output for the same input—and never cause side effects.

When you embrace purity, testability becomes inherent rather than bolted on.

Example: Working with Time — Pure vs Impure

Example of an impure function:

def timeAfterDaysFromNow(days: Int): ZonedDateTime =   
   ZonedDateTime.now().plusDays(days)

The result changes every time you call it. Testing becomes painful.

Example of a pure or total function:


def timeAfterDaysFromNow(now: ZonedDateTime, days: Int): ZonedDateTime = 
   now.plusDays(days)

Now the behaviour is deterministic and the tests are trivial.

This small change is foundational: testability and reproducibility emerge naturally.

Four Principles for Verifying Modern Software

Across multiple organisations and large-scale systems, we apply four architectural principles, each strongly influenced by FP thinking:

1. Design for Failure

Assume components will break. Design systems that behave predictably under stress or partial outages.

2. Testability

Systems must be easy to test in isolation, composition, and in production-like conditions.

3. Reproducibility

If something happened once, we must be able to replay it exactly. This is essential for debugging and regression analysis.

4. Observability

If we cannot see what the system is doing, we cannot trust it.

These form the foundation upon which these FP-inspired techniques sit.

Regression Testing Using Pure Functions

At one client, Machine Learning (ML) models were used to generate user profile attributes (e.g., bot likelihood). The architecture relied on:

Deterministic ML outputs for the same input
A profile-building component that was commutative (order of inputs shouldn’t matter)
An idempotent API (reprocessing shouldn’t change the outcome)

Because these guarantees held, we could simply persist inputs and outputs under a transaction ID and replay them using newer model versions.

This made regression testing cheap, systematic, and extremely reliable.

We’ve used this method with three different clients, with consistently low defect leakage into production.

Property Testing — Discovering Hidden Truths About Your System

Unit tests check examples. Property tests check behaviours.

Properties often reveal assumptions we didn’t know we were making. Especially in sorting, merging, serialising, or composing data.

Common properties include:

Invertibility (e.g., JSON encode → decode → original value)
Idempotency (running an operation multiple times yields the same result)
Commutativity (order of inputs shouldn’t affect results)
Invariance (sorting shouldn’t lose elements)
Stability (equal elements keep their relative order)

Example: JSON round-trip property

forAll { (player: Player) = 
  player.asJson.as[Player] mustEqual Right(player)
}

These techniques reveal subtle issues such as unstable sorting, problems that are hard to detect in conventional tests but can have major downstream consequences (pagination inconsistencies, UI confusion, fairness issues, etc.).

Shift-Left Testing: Verifying Systems Before They Exist

Shift-left testing means testing early, not simply “more”.When designing distributed systems ( streaming pipelines, account migrations, or multi-service workflows) waiting for end-to-end integration is too slow and too risky.

Instead, we:

Model each component using pure interfaces
Provide test-friendly entry points
Validate behaviour before infrastructure is in place
Replace missing services with property-based simulations
Gradually move tests “rightward” as infrastructure matures

Example: Account Migration

A real-world migration pipeline involved:

An API surface
A callback processor
A persistence layer (e.g., DynamoDB)

By isolating the functional core, we could:

Test merge logic without the callback

Test merged is triggered via an event

Test all the components working together

This dramatically shortened the feedback loop and surfaced issues months before full integration.

Real Results

Across multiple clients, these practices led to measurable, long-term outcomes:

17 bug tickets in a 52 week timeframe(for a live, high-traffic system)
Extremely low critical defect rate
Smooth onboarding for engineers of any seniority
Multiple production releases per day
Over 600 user sessions per hour with no major incidents

Testing and design reinforced each other: FP principles created predictable systems, predictable systems enabled deeper testing, and testing revealed new design insights.

Challenges - Because Nothing Comes for Free

Even with these wins, there are trade-offs:

Test pipelines become slow
Flaky integration tests (because network is unreliable)
Maintenance cost is high (~4 lines of test code per line of production code)

But the tradeoff is usually worth it: reliability, reproducibility, and observability are the pillars that allow us to ship with confidence.