Cascading Style Sheets in HTML

What is CSS and Why Cascading?

CSS is an old but gold technology, where styles can be defined in a central style sheet and used across multiple web pages. Cascading refers to the hierarchical logic implicit in the style sheet. A style applied to a parent element will also apply to all child elements of the parent.  For example, if body text of a paragraph is blue, any other elements in that paragraph also inherit blue unless explicitly overriden.

Alternatives to Separate Style Sheet (Inline CSS using style attribute)

A separate style sheet file is the preferred option for maintainability. However there are other ways of using CSS within a specific file. For example, an inline CSS can be used to apply a unique style to a single HTML element, using the style attribute.

<h1 style="color:blue;">Blue heading</h1>

<p style="color:red;">Red paragraph</p>

ssh -T

Recap on ssh, what it is and why it exists

Mastering ssh is essential to connecting into remote servers.

ssh is used to connect to a remote server using the syntax:

ssh [username]@[hostname or IP address]

Explanation of -T flag, and why it makes sense for testing GitHub logins

When you do:

ssh -T 

it means do not allocate a terminal (TTY), so you are asking to connect, but without the interactive shell. 

Connecting to some external services like GitHub operate in such a way that they do not provide shell access. You can still check/test SSH authentication:

ssh -T git@github.com

GitHub should respond with text like:

Hi your_username!  You've successfully authenticated, but GitHub does not provide shell access.

This proves your SSH key was accepted , GitHub recognised your account, future Git operations over SSH should work.

Some Technical Notes on TCP Ports for ssh

Technical note 1: Port 22 is the default TCP port used by SSH for encrypted remote login, command execution and file transfer, as registered by IANA and used by all major SSH implementations.

Technical note 2: IANA - Internet Assigned Numbers Authority

Design Patterns in the Cloud

There are a number of design patterns that have emerged and evolved in cloud computing. Microsoft Learn covers off quite a few of those.

Among the common ones you should know are Ambassador, Circuit Breaker, CQRS, Idempotent Consumer, Sharding and Sidecar.

The CQRS Pattern

CQRS aims to overcome certain challenges with implementing CRUD operations (the typical database operation: create, read, update and destroy).  It stands for Command Query Responsibility Segregration. 

Write operations are abstracted into Commands

Read operations are abstracted into Queries

The idea is, as applications scale, read and write operations often have different performance and scaling requirements. Traditional CRUD architectures do not take this asymmetry into account, which can result in challenges - such as:

Data mismatch - read and write representations of data often differ. Some fields needed during updates may be unnecessary during reads.

Lock contention - parallel operations on the same data set can cause lock contention.

Performance problems - the traditional approach can negatively impact performance due to load on the data store and the data access layer and the complexity of queries needed to retrieve information.

Security challenges - can be difficult to manage security when entities are subject to read and write operations.

Sidecar Pattern

Sidecar Pattern: Introduction

The sidecar pattern is a bit like "aspects" in aspect-oriented programming.  

So your primary application with core functionality runs in its own bubble, and your "sidecar" deals with peripheral tasks (like logging, performance measurement, proxying to remote services). 

Sidecars can be written in a different language to the primary application. 

The most common implementation of this pattern is in containers, where you have sidecar containers, also known as sidekick containers.

Sidecars in Kubernetes

Sidecars in Kubernetes are secondary containers that run along with the main application container within the same pod. These containers enhance or extend the functionality of the primary app container providing services like logging, monitoring, security or data synchronization without altering the main app code.

They can be started and stopped independently of the main container.

Further details, including notes on sidecars and pod lifecycle, can be found on the kubernetes docs website.

MSIX Architecture

For deploying applications to the Microsoft Store, the MSIX format is something you need to very familiar with. It is the wildly successful successor to the MSI format.

Start by reading the Overview on Microsoft Learn.  

For additional background you can read the Microsoft guide to packaging and deployment for Windows Applications. The latter will recommend Microsoft Store as the recommended distribution path for most developers.  Other avenues will require additional certificate signing obligations (and concomitant costs).

One of the first concepts the would-be MSIX master must learn is that of package identity. When your app is packaged as MSIX, Windows assigns an identity to it based on manifest information such as name, publisher, version, architecture and resource identifier (you find this in the AppManifest.xml).

One of the merits of MSIX usage is reliable install and uninstall. On the uninstall piece, it guarantees no leftover files or registry entries. On the install piece, it has a reported 99.96% install success rate.

Containerized execution is one of the more interesting aspects of MSIX. Apps run in a lightweight container with virtual file system and registry. An overview is here.

The Azure Tenant Concept

An Azure tenant is the security and identity boundary for an organization within Azure.

In AWS the Azure notion of tenant broadly corresponds to an AWS organization. 

Within the tenant you have subscriptions. You may bifurcate your subscriptions into production and non-production.

Tenants are endowed with a unique Tenant ID, a globally unique GUID that identifies your tenant across Microsoft services.

Set up Artifact Signing Quickly

 Quickstart: Set up Artifact Signing | Microsoft Learn

Useful Azure Shell Commands

 az account list --output table

will give you a list of subscriptions (the table command line flag tells the shell to convert scraggly-looking JSON to a smarter-looking tabular format).  Subscriptions will display their name, cloud name (e.g. AzureCloud), Subscription ID, Tenant ID, State (Enabled?) and the IsDefault flag.

Copilot Integrated into Azure (Portal)

Copilot is integrated into the Azure portal, and sports a number of agents to help you. 

For example, the Troubleshooting agent exists to help you diagnose problems. To some extent, having a natural language interface may appear liberating, but technical language is still required to operate/co-operate with the agent, for example providing context around Azure resources, resource groups or subscriptions. Azure VMs and Azure VM scalesets (VMSS) are supported.

Stacked PRs - Was Ist Das?

A crazy concept from GH fully detailed here.

Cloudflare on RAG - Hello AutoRAG

This came out in April 2025. Create an AutoRAG instance and point it at a storage location like R2. Simples. Don't craft RAG yourself.

ss (socket statistics) versus netstat

netstat is used in Windows with roots in Unix. In the Linux world, ss is more used than netstat.

ss displays "socket statistics" and is used to "dump socket statistics" as per its description. 

Unlike netstat, ss talks to the Linux kernel directly. 

Used without arguments, ss displays non-listening connections - so an nginx server simply listening for connections would not appear in the output, but an established connection (TCP for example) would appear.

To display listening connections also, do ss -l.

ss -lt
ss -lu

Restricts output to TCP and UDP connections.

Please note: using ss in a WSL shell will only give you the connections relating to the shell and not the wider Windows system in which the shell is running. 

You will still need netstat from a cmd.exe to see the networking connections in Windows. Note that WSL1 shared more of the Windows networking stack than WSL2.

The Markdown Guide

Here is the Markdown Guide, explaining why Markdown is popular. 

Markdown was created by John Gruber in 2004.

openssl rand

openssl rand is an OpenSSL command that generates cryptographically secure random bytes using the library's CSPRNG (cyptographically secure pseudorandom number generator) with options for raw, hex or Base64 output.

Example usage:

openssl rand -hex 16

openssl rand -base64 16

The number at the end states the number of bytes to generate. 

The GitHub location for OpenSSL can be found here. This also has extensive documentation in Markdown.

Learn more about OpenSSL here from the OSSL Guide. An interesting application of OpenSSL's capabilities is implementing systems using QUIC (a modern transport layer protocol built on UDP).

From "process containers" to control groups

The Linux feature of control groups (or cgroups) originated in what was originally called "process containers". cgroups are a Linux kernel feature.

Read the Kubernetes (K8s) Source Code

The Kubernetes source code is available on GitHub.

In addition to reading the source code, it is useful to consider the intellectual origins of K8s in "Borg".

It is often portrayed as the "spiritual" open source successor of Google's Borg, a cluster manager running hundreds of thousands of jobs, across thousands of applications, running on clusters each of tens of thousands of machines.

The Borg paper covers how shortcomings in Borg were addressed in the design of Kubernetes (this is worth understanding/being aware of). There is an overview here from ACM Queue called "Borg, Omega and Kubernetes" (Omega was an offspring of Borg).

(Historical note: Borg in turn was the successor of two internal Google systems, Babysitter and Global Work Queue, both of whose design predated the introduction of Linux control groups).

The Borg paper also mentions the Google Container Enginer (GKE), which is a Google-hosted version of Kubernetes.

What Linux version runs in your WSL shell?

lsb_release -a

LSB modules are components defined by the Linux Standard Base. They specify standard libraries, commands and runtime behaviours - ensuring compatibility across Linux distros. The LSB project is led by the Linux Foundation.

Does Devin Do The Trick

Devin (from Cognition) is billed as the world's first autonomous software agent. But does Devin do the trick? Can it solve some of the thorny problems in agentic programming?

Logos using or trialling Devin include (in banking) Citi, Goldman Sachs, Santander, itau (in tech) openrouter and servicenow, (in media and telco) Fox, AT&T and (in startups) Modal.

Control-Shift-Escape

This is your shortcut to Task Manager. Use it periodically to build intuition about system resource usage.

Protocol Downgrades

Protocol downgrades, also known as downgrade attacks, bidding down attacks and rollback attacks, is when a computer system is coaxed into abandoning a high quality mode of operation in favour of a lower quality mode of operation.

A historical example was a flaw in OpenSSL that enabled an attacker to use a lower version of TLS between client and server.

What is HSTS?

HSTS is HTTP Strict Transport Security. This is a web security policy defined under RFC6797 forcing browsers to use HTTPS only. This protects users from attacks like protocol-downgrade and cookie hijacking.

Internet Gateways (IGWs) In Depth

All WinJoes know what an internet gateway is. Many affectionally refer to these as IGWs. But few know what these gateways do in amazing depth.

We aim to bridge that gap and confer, dare we say it, in-depth knowledge. We educate the new generation of "gateway gurus", or "IGW gurus".

So one question for you - NAT. How do IGWs interact with NATs - if at all? Does this differ in AWS versus other clouds? Exercise for the reader.

Subnets are Routing Boundaries not Security Boundaries

AWS, as well as other cloud providers, use subnets to partition virtual networks (e.g. in AWS VPC - Virtual Private Cloud).  

These subnets divide up the IP address space into separate compartments for routing traffic.

In AWS, another way of saying this is "each subnet is a slice of your VPC's CIDR block".

Each subnet block in AWS is tied to a particular AZ, or Availability Zone. Subnets cannot span AZs and this preserves the availability pattern (e.g. one private subnet per AZ).

There are many types of subnet in AWS.  Examples are:

• Public subnet - subnet has a direct route to an internet gateway. Resources in the public subnet can access the public internet.
• Private subnet - subnet has NO direct route to an internet gateway. Resources in the subnet require a NAT device to access the public internet
• VPN-only subnet - the subnet has a route to a Site-to-Site VPN connection through virtual private gateway. The subnet has no route to an internet gateway
• Isolated subnet - not connected to the internet - in fact, no routes to destination outside its VPC
• EVS subnet - a type of subnet created by Amazon EVS (very specific to VMware)

(Sidebar: internet gateway - bridge ("network bridge","network component")  between private network and the internet,enabling traffic routing, protocol translation, NAT, DHCP and security filtering)

Choosing Network Size in AWS - Forward Slash Notation

Network size (in terms of IP address ranges) in AWS is specified using CIDR notation. 

(Sidenote: CIDR stands for classless interdomain routing, which replaced the now obsolete classful networking architecture which prevailed from 1981 to 1993, when CIDR was introduced.  If you are interested in the classful system have a look at RFC 791 which covers IP and describe the class system).

Example:

192.162.1.0/24

The forward slash 24 means the first 24 bits are fixed.  The rest (i.e. last 8 bits) are flexible.

From the AWS documentation: 

"When working with networks in the AWS Cloud, you choose your network size by using CIDR notation. In AWS, the smallest IP range you can have is /28, which provides 16 IP addresses (2^4). The largest IP range you can have is a /16, which provides 65,536 IP addresses (2^16)."

AWS Global Infrastructure and Services

AWS Regions and Availability Zones

AWS Service Endpoints

AWS Services by Region

Python secrets module

The secrets module in Python is used to generate cryptographically strong random numbers.

This should be used in preference to the random module, for modeling and simulation, not cryptography.

The background -

Random numbers are used in cryptographic applications e.g. in key generation, initialization vectors and nonces, and salts in certain signature schemes.

One-time pads also require a truly random source.

Hennessy and Patterson - The "HP" Book

You know if you know.

The "HP Book's" Take on Parallel Processing

Parallelism at multiple levels is a driving force of computer design.  

Belief in that driving force, in pushing it forward, in harnessing it for the progress of humanity - is essential for the computer-oriented changemaker.

Fundamentally applications have two types of parallelism - the data-level and the task-level. Data-level parallelism is what makes GPUs so powerful.

Computer Architecture: A Quantitative Approach

Computer Architecture: A Quantitative Approach is a constantly-updated "classic" of computer science. 

It is written by authors John Hennessy and David Patterson.  It is thus sometimes referred to in certain circles as the "HP book".

John Hennessy developed one of the first commercial RISC microprocessors. He received the Eckert-Mauchly award (IEEE Computer Society) in 2001 for contribution to RISC processors.

David Patterson has been teaching computer architecture at UC Berkeley since 1977 and has received a Distinguished Teaching Award from the University of California.

One of the reviews of the 5th Edition (published in 2012) praise its:

           "revised chapter on data-level parallelism, which demystifies GPU architectures".

James Hamilton of Amazon Web Services (Distinguished Engineer) compares the book to a "fine wine".

Making Programs Fast on Modern CPUs

A great GitHub resource on "making programs fast on modern CPUs".

HTTP 429

When a client request exceeds the number of requests allowed in a certain time frame.

Apache Airflow

Apache Airflow is a popular tool with data engineers.  

With it you can programmatically create, schedule and monitor workflows. It's kind of "workflow-as-code". 

Pipelines are defined in Python, can can be built dynamically. There is good cloud integration.

Airflow also makes use of the Jinja templating engine.

It also has a command-line interface (Apache Airflow CTL, or airflowctl) that interacts exclusively with the Airflow REST API.

Incautious Experiments of the AI Labs

Cal Newport (of "Deep Work" fame) makes the excellent point of AI labs being guilty of "incautious experiments" to trump up the significance of their work - specifically a "narrow band of incautious experiments" which the "frontier labs" have executed.  

He argues for specificity on what experiments they are running and move away from thinking of AI as a "singular technology on an inevitable, fixed trajectory".

He covers this in the blog post "It's time to investigate the AI Labs".

P99 Latency and its Significance

P99 latency (or 99th percentile response time) - refers to the 99th percentile of request response times - in other words, the "slowest  1% of requests".

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. 

Codex Terra Light 5.6 on the ChatGPT Application

A lightweight coding model (Codex Terra Light 5.6) is available in the ChatGPT app. It is ok - and can do very simple refactoring when you know the approach you want to take.

The .vs hidden directory

Visual Studio creates a .vs directory at the root of your solution. It is used to store solution specific settings and temporary data to help manage the state of your development environment. Fine to .gitignore.

However one interesting directory you may find inside is a slnx file. 

A slnx file is the XML version of the traditional sln file. However what is in .vs are supporting files for the slnx file format rather than the file itself.

Service Status Pages

The MSVS Service Status page is powerd by Atlassian Statuspage. It is free for up to 10 users.

Visual Studio 2026 August Release Notes

Among the changes in MSVS August release are thinking levels for GitHub Copilot - low, medium or high - with the highest obviously burning most tokens.

Low is for simple code suggestion; high for hard-to-debug issues.

There is also Git Agent that can be used to review your code prior to a pull request.

MSVS runs on monthly feature updates.

EC2 instances have different specializations - choose type and size

EC2 instance types are grouped under instance families. These may be broadly classified as general purpose and optimised forms.

More granualrly, these include general purpose, compute optimized. memory optimized and "supercompute" i.e. GPU powered/"neocloud" powered.

General purpose are a good starting point.

Compute optimized are good for machine learning (a compute intensive task). Gaming servers also would benefit from compute optimized EC2 instances, as would high performance computing and scientific applications.

Memory-optimized is good for applications that use large data sets in-memory. This differs from storage-optimized for workloads that utilise a great deal of locally stored data.

Accelerated-computing instances are good for floating point number calculations, graphics processing and pattern matching. They use hardware accelerators (like GPUs).

After choosing instance type, choose instance size. 

Performance and cost should be key parameters here.

AWS Compute uses Multi-Tenancy

EC2 instances are virtual machines (VMs). VMs share an underlying physical machine with other instances (this is called multi-tenancy).  This is enabled by software called a hypervisor. VMs are isolated but share resources.

When you provision an EC2 instance, you can choose the operating system as Windows or Linux. You can provision thousands of EC2 instances on demand. They are resizable so you can start small and then give your instance(s) more memory and CPU.  This is the "elastic" nature of EC2 and is known as vertically scaling an instance. You can also control networking in EC2. Essentially you can choose what requests get to your server.

Virtualization is not a new concept; but AWS makes it more convenient to acquire servers via its Compute-as-a-Service model.

Compute Conceptualized in Terms of Power

Compute can be conceptualized in terms of power - in that it can be defined as the processing power needed to run applications, process data and and do calculations - and in the cloud, this is power "on demand". 

Thus power, and it's availability, is strategically important for cloud providers' expansion. 

Amazon's Elastic Compute Cloud (called EC2 for the double-use of the C) is the epitome of this definition of compute, and represents a powerful compute service from AWS.

iPhone Low Data Mode Explained

Some Windows users also have iPhones and need to understand iPhone settings and usage. In this spirit we deep dive Low Data Mode on the iPhone.  This can be a good option when travelling.

Low Data Mode is a Data Roaming setting. 

Settings -> Mobile Service -> Mobile Data Options -> Data Mode -> Low Data Mode

Other options in this category are Allow More Data on 5G and Standard.  Standard allows automatic updates and background tasks on mobile data, but limits video and FaceTime quality.

VPS Errors on Random Websites

Suggestive of problems with virtual private servers (a virtual machine hosted in a DC, with a dedicated operating system- typically Linux or Windows, root/admin acces and the ability to run websites, databases, APIs or background services).

AI Orchestrators

LangChain, CrewAI, AutoGen, ADK and LangGraph are examples of tools used for agent orchestration.

RAG with Pinecone and Chroma

Pinecone (pinecone.io) is "the knowledge engine for agents" - aka. a vector database for RAG pipelines.

Chroma is open source search infra for AI - also built on vector database technology.

Prompt Optimization - Worth the Investment

Prompt optimization involves trying various prompts to find the most effective prompt for an LLM. 

This kind of A/B testing, or A/B/C/D.. testing is going to burn tokens. It may be justified in some regulated domains where you need to show consistency.

The ideology is that even if you express your intent well, the LLM underneath may not produce the best output with your input. This is because (it is said) "being clear" is not the same as "being optimal" for a generative model.

AutoPrompt is one option for what it refers to as "prompt tuning".

DSpy (a Python framework for building AI systems) has also been used for the same use case.

A video on DSpy can be found here.

Generative Models - GANs/VAEs and Diffusion Models - O My

 GANs are obviously generative adversarial networks. 

• Developed by Ian Goodfellow and colleagues in June 2014
• In this construct, two neural networks compete with each other in the form of a zero-sum game, where one agent's again is the other agent's loss
• The concept is that competition forces both to get better
• The game is to provide high realism output
• They are used where you need hi-fidelity synthetic data, realistic imagery
• They are not the dominant model for consumer generative AI
• The theory behind GANs is an interesting application of probability spaces

Diffusion models.

• Class of latent variable generative models
• Based on diffusion processes in applied probability
• The goal of the model is the learn the diffusion process that underpin an image (strange concept in itself, and one that puts this technique in the realm of latent variable generative models)
• Two components - the forward diffusion process and the reverse sampling process
• Simple example of a diffusion process is ink dropped in water, droplets diffuse through the water
• One example application is denoising images (where image is blurred with Gaussian noise)
• Stable Diffusion and DALL-E are diffusion based image generators

VAEs are variational auto-encoders

• A variational auto-encoder (VAE) is an artificial neural network introduced by Kingma and Welling in 2013
• It is part of the families of probabilistic graphical models and variational Bayesian methods

** classes of model **

Latent variable generative models.

• Statistical model that relates a set of observable variables (also called manifest variables, indicators) to a set of latent variables
• Latent variables are those that can be observed /inferred only via a mathematical model
• They may correspond to aspects of physical reality
• Earliest reference: Francis Bacon, Novum Organum
• It may reduce the dimensionality of the data

Auto-encoder.

• Form of artificial neural network.
• Used to learn efficient codings of unlabeled data (unsupervised learning)
• An autoencoder learns two things:
• Encoding function - transforms the input data 
• Decoding function - that recreates the input data from the encoding/encoded representation
• Autoencoder learns an efficient representation (encoding) for a set of data, typically for dimensionality reduction, to generate lower dimensional embeddings for subsequent use by machine learning algorithms

Variations of auto-encoders that embody useful properties.

• Example: regularized auto-encoder (aka sparse, denoising and contractive autoencoders)
• Example: variational auto-encoder (used for generative applications)

"A continued process which... escapes the observation of the senses" - Francis Bacon

xcopy still works

You can still do a mean recursive copy in cmd.exe using:

xcopy *.* /s

But when copying to a target directory, make sure the directory exists, or it will create a file (as it has done consistently in previous versions).  

MS-DOS is still alive and well.

The Codex Incompleteness Theorem

A few Codex gaps with workarounds.

Codex will create a .git directory - but without initializing. Before you check in code, do a git init.

For Windows, IDE based builds won't work - as settings need to be done in the GUI to persist in config. This makes debugging from the IDE difficult - "if I change settings in IDE for my ease of debugging will it break build process used by Codex?"

OAuth2 - Read the RFC

Given its widespread usage, it is worth reading the OAuth2 specification (RFC6749). OAuth2.1 is in development to integrate the OAuth2 spec with common extensions.

Entire

Entire is a new developer platform which boasts "every agent session/decision/tool stored in your repo". It aims to be the GitHub equivalent for agentic development.  Accessing Entire requires giving it access to your GitHub repos with authentication via GitHub OAuth (which uses OAuth2 - the current industry standard protocol for authorization).

Statistical Similarity

KL divergence is a way to measure "closeness" of two probability distributions. It is used in the literature on model cloning/model distillation.

Another name for it is "relative entropy".

Its full form is Kullback-Leibler divergence. 

It is denoted D[KL]( P || Q ). P is the true probability distribution and Q is the approximating probability distribution.

Mathematically:

D[

Time Synchronization in Distributed Systems - A Different Take

Distributed systems employ a lot of synchronization - data synchronization (get all nodes consistent on data) as well as time synchronization (so every node has the same view of time).

Time synchronization can be achieved via protocols like NTP and PTP (the latter is precision time protocol - for applications like high frequency trading), but also logical systems like Lamport timestamps which order events without relying on physical time.

Lamport timestamps are a logical clock mechanism to capture chronological and causal relationships in a distributed system. Leslie Lamport introduce this as far back as 1978.

A variation of logical clock known as a vector clock is used in a variety of distributed database systems.

Revisiting Refactoring -> Purpose - "Confidence in Code"

Martin Fowler's book "Refactoring - Improving the Design of Existing Code" (with contributions by Kent Beck), first published in 1999, is really interesting and deserves a revisit in the context of AI.

On the cover of the Addison-Wesley Second Edition, he is quoted as saying: 

"Any fool can write code that a computer can understand. Good programmers write code that humans can understand".

Erich Gamma (one of the "Gang of Four" behind Design Patterns) remarks in the preface that refactoring began in "Smalltalk circles" and found its way into other programming language camps. 

He also emphasises its core role in framework development. 

"Frameworkers know that a framework won't be right the first time around—it must evolve

as they gain experience...The key to keeping code readable and modifiable is refactoring—for frameworks, in particular, but also for software in general." - Erich Gamma

Erich expands on the risk of refactoring - the fact it can set you back days or weeks and "refactoring becomes riskier when practiced informally or ad hoc".

Erich emphasises that a system is needed for successful refactoring: "To avoid digging your own grave, refactoring must be done systematically".

He mentions the core of the book is a "comprehensive catalog of refactorings".

He also relates a coding session with Kent Beck involving disciplined "one step at a time" refactoring and how we felt afterwards - 

"Not only did my confidence in the resulting code increase, I also felt less stressed."

A Note on LSTM

LSTM, or long short term memory, seemingly paradoxically named, was co-invented by German computer scientist Sepp Hochreiter, who incubated it in his 1991 diploma thesis leading to its main publication in 1997. 

LSTM addresses the problem of numerical instability in training recurrent neural networks (RNNs) that prevent them from learning long sequences (the so-called vanishing gradient problem).

In 2007, he and others applied LSTM, optimizing the architecture, to very fast protein homology detection without requiring sequence alignment.

Protein homology detection is the process of identifying whether two proteins share a common evolutionary origin - one of the core problems in computational biology.  

Homology implies shared structure and shared function.

Agentic Coding, IDE Debugging

You've built your software agentically. Now you want to (need to) debug it in an IDE.

You may need to add some extra settings.

OpenAI's Astra Solves More Maths Problems

Astra has solved 10 hard maths problems (published 1 August 2026) following on from its disproof of the Erdös unit distance conjecture (from combinatorial geometry) in May 2026.

A paper of almost 250 pages (inclusive of references) is available from OpenAI's website.

Defensive Perl

Perl is less fashionable than Python these days, but it is a very flexible language which excels in text processing.

Its flexibility allows a myriad of programming styles, however, so having a set of defensive techniques helps.

Here are some top tips:

• Switch warnings on - use the minus-w command line flag -  #! perl -w
• Learn and use perlpod - it looks a bit like this at the start of your file  =head1 NAME  myscript =cut
• Always use strict; at the start of your program (this pragma restricts expressions that are hard to debug)
• Qualify your variables with type prefixes (similar to "Hungarian" notation) e.g. my $sHeader for strings, my @aCodes for arrays, my %hCodesToDescriptors, and appropriate equivalents for common custom types

Recap on pragmas: A pragma is a module which influences some aspect of the compile time or run time behaviour of Perl, such as strict or warnings. From Perl 5.10 onward - custom pragmata are supported.

Happy Perling!

How Imports Work in Python

The syntax for import is as follows (keywords in quotes):

"import"  module [ "as" identifier ]

There is also a variation to use when testing proposed changes to Python:

"from " "__future__" "import" feature [ "as" identifier ]

The first thing import does is find an load the module. It then initialises the module.

Frozen Frames when Debugging Python

When running pdb, you will notice certain debugging frames as frozen.  This is typically when:

• code is compiled C-extension code (e.g. importlib, asyncio, threading internals)
• the debugger cannot step in or modify them
• they are part of Python's frozen importlib bootstrap

For example, in the following:

<frozen importlib._bootstrap>

<frozen importlib._bootstrap_external>

The modules are embedded in the Python binary.

If you try ll in the Python debugger when compiled code is being processed, you will get the error: *** could not get source code.

Understanding HTTP State Management

HTTP state management is covered in RFC6265.  

Python's request module however refers to its predecessor RFC2965 within the class DefaultCookiePolicy in cookiejar.py. Some programmers say the implementation is quite strict.

One difference in the RFCs is the use of Augmented Backus-Naur form (ABNF) in the latter, not used in the former. ABNF for specifications is formalised in RFC5234 (an Internet standard, proposed to be augmented by RFC7405).

Understanding HTTP Redirects

Introduction

If you want to program an HTTP request module (to make HTTP requests, to download web pages, or other data) there are a number of relevant concepts relating to HTTP that you must understand.

One of these concepts is HTTP redirects. What are they, why do they exist, and what a "reasonable" number of redirects looks like when sending an HTTP request to a server.

What is a redirect - technically speaking?

First the technical part. HTTP redirects occur when a server responds to a client request with the reply 3XX (status code). This is coupled with a location header of the URL it wants the client to load instead.

The browser or other HTTP client (which could be a Python program, for example) then follows the redirect, issuing a new request to the URL in the location header.

Why are they needed?

Examples:

301 Permanent redirect - e.g. for site reorganization, domain migration, SEO link preservation

Also temporary redirects - e.g. for load balancing

HTTP to HTTPS redirect

Redirects can be configure in Apache .htaccess and in nginx.

Pythons requests module allows by default 30 redirects.

PyCharm

PyCharm is an IDE for Python development from JetBrains. Copilot recommends this for large projects.

However to connect to WSL projects you need to have the JetBrains gateway installed.

Know your requirements well to understand if you really need such an overwhelming IDE.

Epigrams on Programming by Perlis: Seek Symmetry Everywhere

The echo of Alan Perlis' insights reverberate in computer science departments around the world, and immortalised in Epigrams on Programming, which he published in 1982. Here is a selection of his well-known aphorisms.

One man's constant is another man's variable.

Everything should be built top-down, except the first time.

Functions delay binding; data structures induce binding. Moral: structure data late in the programming process.

Syntactic sugar causes cancer of the semicolon.

If a program manipulates a large amount of data, it does so in a small number of ways.

Symmetry is a complexity-reducing concept (co-routines include subroutines); seek it everywhere.

A programming language is low level when its programs require attention to the irrelevant.

It is better to have 100 functions operate on one data structure than 10 functions on 10 data structures.

Get into a rut early: Do the same process the same way. Accumulate idioms. Standardize. The only difference (!) between Shakespeare and you was the size of his idiom list - not the size of his vocabulary.

If you have a procedure with 10 parameters, you probably missed some.

Recursion is the root of computation since it trades description for time.

If two people write exactly the same program, each should be put into microcode and then they certainly won't be the same.

In the long run every program becomes rococo - then rubble.

Every program has (at least) two purposes: the one for which it was written, and another for which it wasn't.

A language that doesn't affect the way you think about programming, is not worth knowing.

Wherever there is modularity there is potential for misunderstanding: Hiding information implies a need to check communication.

Optimization hinders evolution.

A good system can't have a weak command language.

To understand a program you must become both the machine and the program.

One can only display complex information in the mind. Like seeing, movement or flow or alteration of view is more important than the static picture, no matter how lovely.

Once you understand how to write a program get someone else to write it.

Around computers it is difficult to find the correct unit of time to measure progress. Some cathedrals took a century to complete. Can you imagine the grandeur and scope of a program that would take as long?

In programming, everything we do is a special case of something more general - and often we know it too quickly.

Simplicity does not precede complexity, but follows it.

Programmers are not to be measured by their ingenuity and their logic but by the completeness of their case analysis.

Everyone can be taught to sculpt: Michelangelo would have to be taught not to. So it is with great programmers.

The most important computer is the one that rages in our skulls and ever seeks that satisfactory external emulator. The standardization of real computers would be a disaster - and so it probably won't happen.

Some programming languages manage to absorb change, but withstand progress.

There are two ways to write error-free programs; only the third one works.

In software systems it is often the early bird that makes the worm.

Sometimes I think the only universal in the computing field is the fetch-execute cycle.

The goal of computation is the emulation of our synthetic abilities, not the understanding of our analytic ones.

Like punning, progamming is a play on words.

As Will Rogers would have said, "There is no such thing as a free variable".

Giving up on assembly language was the apple in our Garden of Eden.

When we understand knowledge-based systems it will be as before - except our fingertips will have been singed.

A LISP programmer knowns the value of everything, but the cost of nothing.

Software is under a constant tension. Being symbolic it is arbitrarily perfectible; but also it is arbitrarily changeable.

It is easier to change the specification to fit the program than vice versa. 

In seeking the unattainable, simplicity only gets in the way.

In programming, as in everything else, to be in error is to be reborn.

When we write programs that "learn", it turns out that we do and they don't.

Often it is the means that justify the ends: Goals advance technique and technique survives even when goal structures crumble.

Is it possible that software is not like anything else, that it is meant to be discarded: that the whole point is to see it as a soap bubble?

Because of its vitality, the computing field is always in desperate need of new cliches: Banality soothes our nervers.

Prolonged contact with the computer turns mathematicians into clerks and vice versa.

In computing, turning the obvious into the useful is a living definition of the word frustration.

We are on the verge: Today our program proved Fermat's next-to-last theorem.

Motto for a reseach laboratory: What we work on today, others will first think of tomorrow.

Computation has made the tree flower.

The computer is the ultimate polluter : its feces are indistinguishable from the food it produces.

When someone says "I want a programming language in which I need only say what I wish done," give him a lollipop.

Interfaces keep things tidy, but don't accelerate growth: Functions do.

Don't have good ideas if you aren't willing to be responsible for them.

Computers don't introduce order anywhere as much as they expose opportunities.

In man-machine symbiosis, it is man who must adjust: The machines can't.

The proof of a system's value is its existence.

You can't communicate complexity, only an awareness of it.

Within a computer natural language is unnatural.

Most people find the concept of programming obvious, but the doing impossible.

#116

Use of Mathematical Induction in Proofs of Program Correctness

Robert Floyd introduced MI as a systematic method to prove the correctness of computer programs in his 1967 paper "Assigning Meanings to Programs", written at the then Carnegie Institute of Technology, supported by DARPA.

This directly inspired Tony Hoare's axiomatic semantics and the development of Hoare logic (also known as Floyd-Hoare logic).

Floyd acknowledges gestation of these ideas by Perlis and Gorm, albeit in unpublished papers.

Mathematics in VS Code with Lean

Formalizing mathematics is now possible in VS Code with Lean. See the manual here. Extension here.

Lean functionality is exposed in the UI via the universal quantifier at the top right of VS code.

Consider copying the MIL folder, containing key examples, so you can tinker with the example code.

MIL = Mathematics in Lean.

When you download the MIL, you will see a flurry of activity in your Output Console in VS Code. This will include reams of stuff relating to "Fetching Mathlib build artifact cache" and thousands of file downloads.

You will also see the incantation "lake build" which is the primary build command in the Lean build system.

Advice on how to work through the MIL textbook from the official website - "working through the exercises is central to the experience".

Note: when reading Lean files in VS code turn off Unicode character highlighting (Control-, to get into settings, and update Text Editor settings).

kdb+ - An Intro

kdb+ is a high-performance time series database and analytics engine powered by a vector language q. It has been in existence for over 30 years.

It uses columnar storage for efficient querying. For example, if you have temperature readings, taken at 5 minute intervals, you can pull out the whole vector of temperatures in a single query (you are pulling the full time series vector as opposed to a reading from a time series).

If you have corresponding humidity readings, you can do a similar query.

This avoids reading entire rows even if only one field is needed. Typical relational databases query cross-sectionally.

Open Source - and Goldman Sachs??

Goldman Sachs has open sourced some of its code.

The Lean FRO Year 3 Roadmap

Changes to Lean - as articulated by Lean FRO's Y3 roadmap.  

Some items will for sure be done, some may be pushed to Y4.

All roadmap content can be found here.

While we are there, let's say thank you to the Lean Team.

The Draw Tab in Word

The Draw tab in the Word ribbon is a great feature - but it may be turned off by default.

To turn it on do the following:

1.    File

2.   Options

3.   Customize Ribbon

4.   Select Draw

This will enable you to use a freeform marker in your Word doc.

Theorem Proving in Lean - What Makes Dependent Type Theory Dependent?

This precis is based on the Lean Manual, Section 2.8.

Zulip

Zulip is an open source chat platform to help distributed teams communicate effectively. The Lean community used Zulip to collaborate.

Lean Ecosystem Decoded

elan - package manager for Lean. elan can be used inside VS code and will manage all versions of Lean on your system

Lake - the standard project structure and build system used in Lean

mathlib4 - the math library for LEAN

mathlib4 can be found here. It contains both programmatic infrastructure and mathematics.

Theorem Proving in Lean - Basics of Dependent Type Theory

The master guide is here.

DTT and its Specific Variant for Lean

Dependent type theory (DTT) allows you to express complex mathematical assertions and reason about them in a "natural and uniform" way. 

Lean is based on a version of DTT called the Calculus of Constructions, with a "countable hierarchy of non-cumulative inverses and inductive types". This sounds complex. 

The following section explains this.

First, let's talk Simple Type Theory

In "type theory" every expression has a specific type. e.g. the expression x+0 may denote a natural number in a specific context. In another context, it may be a floating point number, of a particular precision.

In Lean, a natural number is an arbitrary precision unsigned integer.

Our use of the arbitrary precision (unsigned) integer, reflects the unnatural way of thinking about counting numbers from a computing perspective. In computing, we think of the object, but also the memory it occupies - so we speak of 16 bit integers, 32 bit integers and so on - a nod to the physical limitations of computers. n-bit integers where n is not predefined underlies this concept of arbitrary precision.

An arbitrary-precision integer can grow to any number of bits, limited only by available memory. 

This differs from so-called fixed-width integers (8-, 32-, 64- bit).  

A variable-length array of digits/bits are used so it can represent arbitrarily large integers without overflow. (Analogies include - BigInt in Java, or System.Numerics.BigInteger in C#).

Defining Contants in Lean with the def keyword

Let's define some constants in Lean.

/- Define some constants. -/

def  m:  Nat := 1   --m is a natural number

def  n :  Nat := 0

def  b1: Bool := true  --b1 is a Boolean

def  b2: Bool := false

Now check their types using: #check m;  #check n; #check n+0 etc. You can also run some "evals" in Lean: #eval  5*4; #eval m+2 etc.

The def keyword introduces new constant symbols to the working environment. The #check command asks Lean to report their types. The #eval command asks Lean to evaluate the given expression.

Composing New Types from Existing Ones

What makes simple type theory powerful is you can build new types out of others.

For example, if a and b are types, a->b denote the type of functions from a to b, a × b denotes the type of pairs consisting of an element of type a and element of type b.

Note on use of Unicode: (From the Lean Manual): "The judicious use of Unicode improves legibility, and all modern editors have great support for it. In the Lean standard library, you often see Greek letters to denote types, and the Unicode symbol → as a more compact version of ->."

Theorem Proving in Lean - Three Definitions to Get Started

This is an abridged account of Theorem Proving in Lean capturing only the SSPs, or super salient points.

Here are some three starting definitions essential for understanding this topic:

Formal verification - using logical and computational methods to establish claims that are expressed in precise mathematical terms. Example claims - mathematical theorem /hypothesis, claims that pieces of hardware or software, network protocols, security protocols - do what they say they actually do.  The process is "describe your system in mathematical terms" ,then use "theorem proving" to establish truth.

Automated theorem proving - focused on "finding". The "ATP" toolkit includes: resolution theorem provers, tableau theorem provers, fast satisfiability solvers to provide means of establishing validity of formulas in propositional and first-order logic.  Computer algebra systems may be used in concert to carry out mathematical computations.  

Automated reasoning - differs; not as "cast iron" as theorem proving. Automated reasoning is a superset of automated theorem proving, which includes imprecise techniques such as heuristic search and fuzzy logic.

The Lean Programming Language

The Lean Programming language is being used to create a new proof of Fermat's Last Theorem. Some lecture notes from London's Imperial College set the scene.

Theoretical Foundation (DTT)

Dependent type theory (DTT) is the theoretical foundation of Lean (the link provided takes you into the Lean manual and gives a brief intro to the theory) which bears "categorical semantics".

Getting Started with Lean

• The best way to get started in Lean is to read Functional Programming in Lean.
• The next step is to read Theorem Proving in Lean.

Who created Lean

Lean was created by Brazilian computer scientist Leonardo de Moura, in 2013, when he worked in Microsoft Research (where he worked for 16 years). 

Leonardo is now Senior Principal Applied Scientist at AWS, where he works in the Automated Reasoning Group.  This group does a lot of work in Provable Security and Software Assurance.

Lean is available under the Apache 2.0 license.

ngrams, ngrams everywhere

An n-gram is a continuous sequence of n items - words, letters or symbols - from text or speech, used to analyze patterns and predict sequences in language.

Suppose we choose the items of our n-gram as "words". We then have the following taxonomy:

• unigram - consisting of a single word e.g. design
• bigram - consisting of two words e.g. design experiments
• trigram - e.g. design of experiments

Google has a great ngram viewer to see the frequency of certain ngrams in books throughout the ages.

mTLS - building machine to machine trust

What is mTLS? 

mTLS is also known as mutual TLS, after the ubiquitous security protocol. It is used in environments where machine-to-machine trust really matters.

Where in general is mTLS used? Where specifically is mTLS used? Did someone say "Kubernetes service mesh"? I think so! 

It's not generally used for public websites, but inside serious enterprise systems, it's a standard way to guarantee only authenticated services speak to each other.

Examples in modern infrastructure include: Kubernetes service meshes (Istio, Linkerd), API gateways, internal microservices, banking and trading and zero-trust networks.

Is mTLS a standard?

It's a section in TLS standard.

Root Certificates

In cryptography, a root certificate is a public key certificate that identifies a root certificate authority (CA).

Examples of certificate authorities (CAs) include SwissSign.

Root certificates are self-signed and forms the basis of an X.509-based public key infrastructure (PKI). Recall the X.509 is the ITU standard for defining the format of a public key certificate.

Worth reading also is RFC5280 which covers X.509 certificates and CRLs (certificate revocation lists).

Certificate Validation with Certifi in Python

The Python certifi package provides Mozilla's "carefully curated collection" of Root Certificates to validate the trustworthiness of SSL certificates while verifying the identify of TLS hosts. 

It has been extracted from the Requests project.

Parity between Azure and AWS

It is worthwhile to maintain knowledge parity between Azure and AWS. 

If you use a cool thing in Azure, chances are the same functionality exists in AWS (e.g. managed kubernetes service - known as AKS or EKS in respective clouds) and so you should know how to do same cool thing in AWS.

Cloud economics may dictate future decisions.

A Nod to AWS EKS

AWS EKS (Elastic Kubernetes Service) is a fully managed Kubernetes service provided by AWS. 

EKS simplifies deployment and management of containerized applications using Kubernetes. Users need not manage the Kubernetes control plane or nodes manually.

Jargon warning: 

The Kubernetes control plane is the central management utility of a Kubernetes cluster. 

It maintains cluster state, making decisions about the cluster and responding to cluster events. It is made up of several key components that work together.

AWS basically runs the control plane for you.

There are a number of use cases suggested by AWS.

Copliot Studio and Cost Analysis

Copilot Studio is a Microsoft product for building and managing AI agents. 

It has a corresponding licensing guide enabling you to estimate costs of building and running agents with it. At time of writing the licensing guide has been updated in July 2026.

Revisiting Port 443

Port 443 is primarily known for handling HTTPS traffic over TCP, enabling secure communication between browsers and servers.  

It can be used with UDP in specific scenarios like QUIC (for lower latency secure communications) and HTTP/3.

When diagnosing why an HTTPS connection is failing, an in depth knowledge of port 443 is needed.

Visual Studio Community July 2026 Release

See the status of GitHub Copilot from the Visual Studio IDE. Built-in .NET and Azure skills are introduced.

Agent Skills Introduced by Anthropic

Anthropic introduced agent skills which have now been embraced by other vendors too e.g. Microsoft.

Agent skills are a standardized way to extend agent capabilities with specialized knowledge and workflows.  It consists of a folder containing a SKILL.md file.  This contains metadata and instructions for the agent to do its task.

Other stuff can be bundled with the skill as well, as follows.

agents-new-skill/ ├── SKILL.md # Required: metadata + instructions ├── scripts/ # Optional: executable code ├── references/ # Optional: documentation ├── assets/ # Optional: templates, resources └── ... # Any additional files or directories

The PEM Format

PEM (Privacy Enhanced Mail) is a format used for transmitting cryptographic keys, certificates and other data.  

PEM structure consists of a text file in Base64 encoded data format (a binary-to-text encoding consisting of 64 printable characters - the idea is you can push binary data into a communication channel that only supports text). 

Base64 is famous for its use in attachments, since SMTP in its original form was designed to support 7-bit ASCII characters only.

An alternative to PEM in Java contexts is DER (Distinguished Encoding Rules) used for X.509 certificates and private keys.

Busting Certificate Issues in Ubuntu

Suppose you are running a data pipeline on Linux/Ubuntu that consumes data from the web. You get a RuntimeError: "SSL certificate verification failed".  What do you investigate?

Verifying the ca-certificates package and updating /etc/ssl/certs

 sudo apt-get install -y ca-certificates

installs the ca-certificates package (the -y means "say yes to all prompts").

This software processes certificates in PEM format.

With this installed, new certificates can be added to /usr/local/share/ca-certificates.  

The trust store can then be updated with:

sudo update-ca-certificates

You can then check if the certificate has been added.

ls /etc/ssl/certs | grep local-ca

Programming as Play

Shade Zahrai has noted that "play changes your brain". 

Stress drops (cortisol down, dopamine up) when something feels low-stakes and playful.

Daily light-hearted play can train your brain to get comfortable with taking risks, exploring and trying new stuff. It builds a sense of agency, a belief that action can make a difference.  

This concept is also explored in the context of programming specifically in an article on "Hunting the Wiley Hacker" which covers the joy of Linux.

A Scorecard for the AI Age

Is a very nice article by Sarah Friar, CFO of OpenAI, on measuring value from AI.  But how to measure "AI", or do we create measures across every AI vendor/model pair to work out value per segment?

More on Data Validation in Pydantic

Pydantic Validation is the validation layer of the OpenAI SDK, the Google ADK, the Anthropic SDK, LangChain and others.

Pydantic uses Rust under the hood. This makes it faster than say, something implemented directly in Python.

How are the Python and Rust pieces glued together?

The key is that the validation layer is compiled in Rust (pydantic-core).  Data parsing, validation and in general, any perf-critical operations, are done here. Py03 is used to create bindings in Python.

While there is no need to use the Rust code directly, for reference it can be found in GitHub here.

But what does this validation actually entail?  What's the use case?

How does it work?

Type hints (PEP 484) are one of the tools used in Python validation (GvR himself h as co-authored that PEP).  Type hints enable integration with various static typing tools (like mypy) and IDEs (like VSCode).

The Type hints PEP also references PEP 3107 for function annotations (written by Collin Winter and Tony Lownds).

Classical Reinforcement Learning and the Reward Signal

As a prelim to understanding RLHF, it pays to understand classical reinforcement learning, which has been studied under many different guises within computer science and more traditional engineering.

This is concerned with how an agent should take actions in a dynamic environment in order to maximise a reward signal.