Programming "In the Large"

This term (coined in 1975 in a paper "Programming in the large versus programming in the small") refers to programming large-scale software systems.

It embodies principles like modularization, high cohesion and loose coupling, as well as formal project management.

The Browser As Sandbox

A "browser sandbox" isolates pages and scripts in a restricted environment. This can prevent malicious sites from accessing your files and doing other dangerous things on your machine.

Modern browsers run rendering and JavaScript execution in low privilege processes, with a separate "broker process" (or "mediator process") controlling access to system resources (process isolation)  Renderer processes cannot read files, launch programs or interact with other applications.

Types of browser sandboxing include local sandboxing - where the sandbox is built into browsers (Chromium, Firefox, Safari), remote/cloud sandboxing where websites are run in isolated VMs streamed to your machine, and online URL sandboxes (services like Browserling which allow you to open URLs in disposable remote browsers).

Browser sandboxing is a foundational security layer in modern browsers and remote isolation platforms.

One Billion Bytes - It's Not "Big Data"

One billion bytes is not big data.  But it is a big number.  A number equal to 10^9. 

A short form for one billion is giga- in the International System of Units (SI). 

The unit symbol for the gigabyte is GB.

Code 43

Code 43 means Windows disabled a device because its firmware reported a fault. 

You may see it presented thus.

"Windows has stopped this device because it has reported problems (Code 43)".

In fact, the device in question may be perfectly fine.

Ralph Loops

A Ralph Loop is an autonomous agent tool that runs a coding model repeatedly to complete PRDs. 

The concept and inspiration is described by Geoffrey Huntley.

What Scale is Your Big Data

terabytes (TB) - 1000 gigabytes (10^12 bytes) - used in consumer storage

petabytes (PB) - 10^15 bytes  or 1000 TB

exabytes (EB) - 10^18 bytes or 1000 PB

Zettabytes and yottabytes are even bigger measures of memory.

Marker Icon in Microsoft Word

The "marker icon" on the Font group in the Ribbon is what determines background (highlight) colour. It can be hard to identify when the background colour is set to grey and thus blends into the ribbon.

Think of Programming as a Martial Art

Something that requires continuous practice and continuous learning.

Databricks Apache Spark-Oriented Origins

It is enlightening to reflect that Databricks grew out of the AMPLab project (AMPLab was an acronym for Algorithms, Machines and People Lab) at UC Berkeley which worked on a variety of big data projects.

AMPLab invented Apache Spark, Apache Mesos (for compute cluster management, retired in August 2025, having lost mindshare to Kubernetes which was backed by Google and CNCF) and Alluxio. Of these projects, Spark is currently the most impactful product to come out of the AMPLab project.

It was founded in 2013 and offers a cloud-based platform for data analytics and AI. It operates in Azure, AWS and GCP (the "big three" providers).

Databricks the data "lakehouse" architecture, combining aspects of data lakes and data warehouses for managing structured and unstructured data. The company develops the Delta Lake open source project adding ACID transactions to data lakes. A paper describing the challenge of adding ACID transactional capability to data lakes has been published (Armbrust et al).

To recap: ACID is an acronym which stands for atomicity, consistency, isolation and durability. These properties are used to characterize reliable database transactions and was first expounded in an influential 1983 paper "Principles of Transaction-Oriented Database Recovery" (Theo Harder and Andreas Reuter).

Literacy is a Superpower in Software Engineering

Literacy is literally a superpower in software engineering. It is the reason so many good software engineers are avid readers and definitely not just of technical tomes, but enjoy all sorts of fiction (though science fiction is a particularly popular genre for obvious reasons).

Structured Streaming in Spark

Structured Streaming is the stream "processing engine" in Spark, designed for scalability and fault tolerance.  

It is build on the Spark SQL engine. Pause. This has implications to the programming model.

The "weird element" in Structured Streaming (following on from our comment on SQL engine above) is that streaming computations are expressed like queries on SQL tables (check).

The DataSet/DataFrame API is used.

A crazy case study is presented below.

Suppose you want to maintain a running word count of text data from a data server listening on a TCP socket.  This can be expressed in structured streaming!

Ironically, the most concise representation for this is in R which is least best supported language in Spark.

This is what the Python looks like.

import [STUFF]  ---> from pyspark.sql import SparkSession

spark = SparkSession(  ... .appName("WordCount") ..)

Now we create a streaming DataFrame representing text data received from the server listening on localhost:9999 and transform the DataFrame to word counts.

A quick word on port 9999. Why use this?  It is easy to remember and avoids conflicts with standard ports. Java apps sometimes use it for debugging.

(To check if it is being used: netstat -ano | find "9999").

Scala vs Java - The Duel (Both JVM languages)

Scala and Java are highly compatible as both are designed to run beautifully on the JVM (the JVM spec should be read/re-read periodically for all serious Java enthusiasts).

Scala uses lambda expressions more aggressively than Java. Both use invokedynamic under the hood.

Scala dominates now in distributed systems (Spark, Akka) particularly for data engineering and ML pipelines, as well as high performance back-ends.

The following is a good website to keep up to speed on Java: Dev.java: The Destination for Java Developers.

Mechanics of RDDs - Python Examples

A Simple Map-Reduce Pattern Example

Here are some examples showing the "mechanics" of how RDDs work in Python.

lines = sc.textfile("data.txt")

We shall first count the lines in the text file (our data file).  The line above creates a base RDD from a text file. The data is not loaded into memory - it's just a pointer to a file at this stage.

We then do a line count of the data.

lineLengths = lines.map( lambda s: len(s))

So here we create the array of lengths.  We then apply reduce to distil this to a single number (classic map-reduce pattern).

totalLength = lineLengths.reduce( lambda a, b: a+b )

Due to lazy evaluation, when we do the map operation, nothing is computed. Only once we do reduce, which is an action, is the computation performed with Spark breaking it down to run on several machines.

If we want to use lineLengths again later, we can do

lineLengths.persist()

before the reduce operation, to save the output into memory after first-computation.

Parallelized Collection Example

Parallelized collections are easily created using a special SparkContext method.

data = [1, 2, 3, 4, 5]

distData = sc.parallelize(data)

Once built, this distributed dataset (distData) can be operated on in parallel.  For example, to add up the members of the list we can do: distdata.reduce( lambda a, b: a+b ).

RDD - Regen vs Replication

RDDs are not replicated the way databases typically are replicated. Instead, the transformations converting data between states are memorised.

To make this regeneration efficient, only partitions on lost nodes are recomputed, and assigned to working nodes.

Note: some lineage chains can be very long. In these cases, Spark can checkpoint an RDD to stable storage (HDFS/S3). This prevents "ruanway recomputation".

The Different Definitions of Ground Truth

Ground truth - informally - means information known to be true. It is based on empirical evidence rather than inference.

The origin of the term was in remote sensing literature in 1972 in usage by Nasa to reference data about the earth's surface.

The term has since been hijacked by statistics and machine learning communities with altered semantics.

Why Spark Works - Secrets of its Parallel Processing Powers

A Spark progam consists of a driver program that runs the user's main function and runs several parallel operations on a cluster.   It is a parallel processing engine for data. The data structure that enables this is the RDD abstraction.

RDDs are resilient distributed datasets (perhaps a better acronym could be RDDS?) - a collection of elements partitioned across nodes of a cluster that can be operated on in parallel.  

Clearly, this definition speaks to the distributed dataset aspect, but what about the resilient aspect?  Can we say it is implicit in the "can be operated on in parallel" dimension? 

We need to probe what that actually means, to uncover the "secret" of RDDs. Resilient means data remains correct and queryable in the event that nodes go down (which can happen in the physical world).

RDDs are born as files in the Hadoop system (or any Hadoop-supported file system) or an existing Scale collection. RDDs can be persisted in memory for efficient processing and they are resilient against node failures (this bit needs to be understood better - how is this achieved - redundancy of storage??).

(Footnote - once you probe deeper you will start to see ideas percolating from older frameworks like MPI in C++).

Learning Spark from the Latest Docs

Spark is best learned from the various programming guides. 

Access to these can be found from links on its latest documentation page.

These include a Quick Start, an RDD guide, an overview of Datasets and DataFrames and at least two guides on Streaming (1) Structured Streaming, and (2) the legacy functionality of Spark Streaming. 

MLib is also worth understanding, as is GraphX for graph processing, including graph parallel processing.

In terms of interfacing with other languages, Spark and Python is encouraged, whereas Spark and R is deprecated (through PySpark and SparkR respectively).

You should also be familiar with Spark Declarative Pipelines (SDP).

There is an associated knowledge base around deployment - including making Spark play well with Hadoop, Kubernetes and Amazon Elastic Compute (EC2).

The Oh-My-Pi Coding Agent

The oh-my-pi coding agent (aka omp) is getting more attention.  It is a fork of Mario Zechner's Pi.

Lean - Can we Trust the Trust Engine?

The de Bruin principle - it's all in the Kernel

Once upon a time, in the 1960s, a computer scientist called de Bruijn build a system called Automath. His full name as Nicolaas Govert de Bruijn. It incorporated ideas such as dependent types to make it work.

We call him here a computer scientist, but he can equally be called a mathematician, having made contributions to number theory, analysis, combinatorics and logic, and served as Professor of Mathematics at the University of Amsterdam.

One of the things he studied were sequences now known as de Bruijn sequences. Polish programmer Andrzej Trybulec's Mizar system was influenced by Automath.

De Bruijn came up with the idea of creating a kernel separate from the rest of his system.  This kernel is correctness-validation component of the system - the "rule-checker" if you will. It is like the part of a chess computer that validates legal moves - rather than makes smart moves.

Keeping the kernel separate is known as the de Bruijn principle, joining lots of other artefacts attached to his name (such as the de Bruijn-Newman constant, which is closely associated with the Riemann hypothesis).

What underlying logic to use for the Kernel?

"First order" logic, augmented with axioms of set theory, can serve as a good starting point for a theorem prover/correctness checker.   This approach results in a small kernel but lots of coding for complex mathematics. More complex underlying systems are available, including Higher Order Logic (HOL) and Calculus of Inductive Constructions (CIC). Lean uses the latter, or at least features of the latter, to increase expressivity and make programming easier. Features used include proof irrelevance, quotients and nested inductive types.

Taking one example: proof irrelevance is the principle that given a proposition and any two proofs of the same, the two proofs are (considered) equal. This simplifies type theoretic reasoning.

The result is that Lean has a kernel that is much smaller than Lean itself but verifying it is not trivial.

lean4lean and the "multiple kernel" principle

Creator of Lean, L. de Moura, has advocated the "multiple kernel" principle, strengthening the de Bruijn principle by supporting multiple independent kernels.  Lean 3 thus had three independent kernels, one in Lean, one in Haskell and one in Scala (trepplein). Lean 4 invalidated these kernels. Nanoda, an independent kernel in Rust, was thus commissioned together with procedures to write more kernels.

lean4lean was started by Mario Carneiro, an implementation of Lean in Lean which includes an independent kernel.  Efforts are ongoing to verify kernel correctness.

XSS from an OWASP Perspective

Cross site scripting (XSS) is a dangerous type of attack. OWASP analysis can be found here.

Fermat's Last Theorem Proved in Lean 4: Sept 4, 2026

Read the HTML overview from GitHub - rendered via https://htmlpreview.github.io. 

Overview · FLT in Lean 4

A rival attempt to achieve the same outcome has ended in admitted defeat.

Almost 30K theorems were traversed on the path to the proof. The theorem statement is as follows:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

GitHub only shows raw HTML source (it does not render these in case of XSS and malicious scripts). HTML is always displayed as raw text.

InfoSec Standards - The ISO Story

The primary ISO standards for cybersecurity are the ISO/IEC 27000 family.