William Rusnack BebeSparkelSparkel

The Origins and Nature of Logical Assignment

In formal logic and computer science, two notational conventions express relationships between logical expressions: logical assignment ($:=$) and logical equivalence ($\leftrightarrow$). Understanding their relationship reveals how practical implementation needs shaped mathematical notation.

The Programming Era View

Using Existential Quantification for Internal Variables

One of the most elegant features of mathematical logic is how it handles internal variables - those temporary objects we need while building larger mathematical structures. Understanding how to properly use existential quantification for these variables is useful when writing precise mathematical definitions.

The Problem of Internal Variables

Consider a simple example: how do we formally define function composition? Intuitively, when we compose two functions $f$ and $g$, we need some intermediate set where the output of $f$ becomes the input of $g$. But how do we capture this in formal logic?

Lingually Understanding Logical Equivalence (IFF)

Your brain is a powerful language processor. When you encounter mathematical logic, you can leverage your natural language understanding instead of fighting against it.

Consider the confusingly worded "if and only if" used in sentences to represent logical equivalence. When your encounter "if and only if," your language processing actually halts - it has to switch to logical reasoning to understand the unnatural construct. This switching between language and logic interrupts and thus slows your ability to understand a statement.

But your brain already understands equality through the simple word "is":

Why Do We Design Programming Languages Syntax-First?

TLDR: Most programming languages are designed syntax-first, but this approach leads to semantic compromises and resistance to evolution. Following Lisp's example, we should start with a formal semantic model using structured data formats and let syntax emerge as views into that model. This semantic-first approach enables better reasoning about programs and more flexible language evolution.

The Current Approach

Most programming languages start with syntax design - carefully crafting keywords, operators, and grammar rules that will form the surface-level interface developers interact with. But we have strong historical evidence that this might be backwards.

Historical Precedent

Consider Lisp, one of our most influential programming languages. Over 60 years ago, John McCarthy developed Lisp by first defining a mathematical model of computation based on lambda calculus and recursive functions. The famous S-expression syntax came later as a practica

Designing a Language for Formal Verification: Core Elements

When designing a programming language with formal verification capabilities, the fundamental building blocks must first be established. Through careful analysis, the following essential components and their relationships emerge as the foundation for expressing and verifying program properties.

Primitive Elements

The most fundamental components from which all other elements in the formal

Are Modules Just Functions?

A deep dive into programming language design and abstraction mechanisms

OCaml's sophisticated module system is often touted as one of its standout features, especially when compared to Haskell's more limited facilities. But as we dig deeper into modern programming language design, an intriguing question emerges: are modules fundamentally different from functions, or are they just a specialized syntax for something we could achieve with first-class functions and a richer type system?

Let's explore this by building up from first principles.

The Traditional View

The Subtle Difference Between Quantifier and Predicate Restriction

In logic, we often need to make propositions (P) about a domain but then would like to restrict the domain to specific subsets (S) while reusing the proposition.

Quantifier and Predicate Restriction are the two common approaches to domain restriction, explained below.

IRL Example

Imagine you're implementing type checking in a programming language compiler. You need to verify that "all function calls have matching parameter types" - a seemingly straightforward rule. But how you express this constraint in logic can have profound implications for your compiler's correctness.

	#!/bin/sh
	set -e

	# Default values
	output=""
	pdfdocs=""
	manpages=""
	webpages=""
	sources=""

	#!/bin/sh

	file="$1"
	# Check if file exists
	if [ ! -f "$file" ]; then
	echo "Error: File '$file' not found" >&2
	exit 1
	fi

	# Change to directory containing the file

	#!/bin/sh

	for arg in "$@"
	do
	if [ "$arg" = "-selection" ]
	then
	echo "Error: -selection argument is not allowed in this xclip wrapper. Use xclip directly instead." >&2
	exit 1
	elif [ "$arg" = "-h" -o "$arg" = "-help" ]
	then