diff --git a/README.md b/README.md index a992de6..68b7440 100644 --- a/README.md +++ b/README.md @@ -434,6 +434,12 @@ See [ROADMAP.md](docs/ROADMAP.md#do-278a-sil-3-mapping) for detailed objective m - **[Roadmap](docs/ROADMAP.md)** - Development phases and milestones - **[Contributing](docs/CONTRIBUTING.md)** - How to contribute +### Whitepapers + +- **[hadlink: A Minimal, High-Assurance URL Redirection Service](docs/whitepapers/hadlink.pdf)** - Design philosophy, assurance model, and deployment approach +- **[SPARK as a Design Lens: Beyond Verification in High-Assurance Systems](docs/whitepapers/formal-verification-lens.pdf)** - How writing SPARK contracts shaped architectural decisions as a design-time discipline +- **[From Coursework to Craft: Single-Sprint Projects as Engineering Practice](docs/whitepapers/sprint-projects.pdf)** - How single-sprint personal projects build engineering skills that coursework alone does not emphasize + --- ## License diff --git a/docs/CONTRIBUTING.md b/docs/CONTRIBUTING.md index ce16c1b..29d7262 100644 --- a/docs/CONTRIBUTING.md +++ b/docs/CONTRIBUTING.md @@ -29,6 +29,11 @@ Before contributing, understand the project values: 3. **Infrastructure, not features** 4. **Explicit non-goals matter** +For background on the project's design philosophy, see the [whitepapers](whitepapers/): +- [hadlink](whitepapers/hadlink.pdf) - System design and assurance model +- [SPARK as a Design Lens](whitepapers/formal-verification-lens.pdf) - How formal verification shaped the architecture +- [From Coursework to Craft](whitepapers/sprint-projects.pdf) - Project methodology and engineering practice + --- ## What to Contribute diff --git a/docs/README.md b/docs/README.md index 8e2d902..9f1ac95 100644 --- a/docs/README.md +++ b/docs/README.md @@ -19,6 +19,7 @@ - [Cryptography](#cryptography) - [Toolchain](#toolchain) - [Assurance Model](#assurance-model) +- [Whitepapers](#whitepapers) - [References](#references) --- @@ -325,6 +326,14 @@ See [ROADMAP.md](ROADMAP.md#do-278a-sil-3-mapping) for detailed objective mappin --- +## Whitepapers + +- **[hadlink: A Minimal, High-Assurance URL Redirection Service](whitepapers/hadlink.pdf)** - Design philosophy, assurance model, and deployment approach +- **[SPARK as a Design Lens: Beyond Verification in High-Assurance Systems](whitepapers/formal-verification-lens.pdf)** - How writing SPARK contracts shaped architectural decisions as a design-time discipline +- **[From Coursework to Craft: Single-Sprint Projects as Engineering Practice](whitepapers/sprint-projects.pdf)** - How single-sprint personal projects build engineering skills that coursework alone does not emphasize + +--- + ## References This design draws from: diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 9b9647b..3730243 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -127,6 +127,7 @@ Follow the migration plan: Haskell-only → SPARK extraction → frozen API. - [x] Security considerations - [x] Example integrations - [x] Contributing guidelines +- [x] Whitepapers ([hadlink](whitepapers/hadlink.pdf), [formal verification](whitepapers/formal-verification-lens.pdf), [sprint projects](whitepapers/sprint-projects.pdf)) ### Lock SPARK Interface diff --git a/docs/whitepapers/formal-verification-lens.pdf b/docs/whitepapers/formal-verification-lens.pdf new file mode 100644 index 0000000..b67e0cd Binary files /dev/null and b/docs/whitepapers/formal-verification-lens.pdf differ diff --git a/docs/whitepapers/formal-verification-lens.tex b/docs/whitepapers/formal-verification-lens.tex new file mode 100644 index 0000000..23c3a5d --- /dev/null +++ b/docs/whitepapers/formal-verification-lens.tex @@ -0,0 +1,183 @@ +\documentclass[11pt,letterpaper]{article} +\usepackage[margin=1in]{geometry} +\usepackage{parskip} +\usepackage{hyperref} +\usepackage{listings} +\usepackage{xcolor} +\usepackage{booktabs} + +\lstset{ + basicstyle=\small\ttfamily, + keywordstyle=\color{blue!70!black}, + commentstyle=\color{gray}, + stringstyle=\color{red!60!black}, + showstringspaces=false, + breaklines=true, + frame=single, + xleftmargin=1em, + framexleftmargin=0.5em, +} + +\title{SPARK as a Design Lens:\\Beyond Verification in High-Assurance Systems} +\author{Jacob Seman} +\date{} + +\begin{document} +\maketitle + +\begin{abstract} +SPARK is typically discussed as a verification tool, a way to prove that code satisfies its specification. This paper argues that verification carries a significant secondary benefit, particularly for small infrastructure projects: architectural clarity. Writing SPARK contracts forces the engineer to define boundaries, assumptions, and scope before implementation begins. The act of specifying preconditions and postconditions serves as cognitive scaffolding that shapes design, limits complexity, and produces more maintainable systems. We illustrate this with \texttt{hadlink}, a URL redirection service where SPARK contracts guided architectural decisions from project inception. +\end{abstract} + +% ============================================================================ +\section{Introduction} +% ============================================================================ + +The conventional view of formal verification treats it as a post-hoc correctness check. You write the code, then you write the specification, then the prover tells you whether they match. This framing positions verification as an auditing step, valuable but separate from design. SPARK supports this workflow, but it also supports something else: using contracts as a design-time discipline that shapes architecture as a side effect. + +When you write a SPARK contract before writing the implementation, you are forced to answer questions that might otherwise remain implicit. What can this function assume about its inputs? What does it guarantee about its outputs? What states are unreachable? These questions have architectural consequences. A precondition that requires normalized input implies that normalization happens elsewhere. A postcondition that guarantees a security property implies that the property need not be re-checked downstream. The contract becomes a design document that the compiler enforces. + +This paper explores the architectural effects of contract-first development using SPARK, drawing on \texttt{hadlink}, a URL redirection service where contracts guided design from project inception. The primary value of SPARK remains verification: machine-checked guarantees about program behavior. But the discipline of writing contracts produces cleaner architecture as a welcome side effect, and that effect is worth examining. + +% ============================================================================ +\section{Contracts as Design Decisions} +% ============================================================================ + +Every precondition, postcondition, and type declaration is a decision about what the system can and cannot safely assume. Consider the contract for \texttt{hadlink}'s canonicalization function: + +\begin{lstlisting}[language=Ada] +function Canonicalize (Input : String) return Canonicalize_Result +with + Pre => Input'Length >= 1 and then + Input'Length <= Max_URL_Length and then + Input'First = 1 and then + Input'Last < Integer'Last - 10, + Post => (if Canonicalize'Result.Status = Success + then To_String (Canonicalize'Result.URL) = Input and then + Is_HTTP_Or_HTTPS (Canonicalize'Result.URL) and then + Not_Private_Address (Canonicalize'Result.URL) and then + No_Credentials (Canonicalize'Result.URL)); +\end{lstlisting} + +This postcondition is not just a correctness check. It is a design statement: on success, the output preserves the input exactly, and four security properties hold. Every downstream consumer can rely on these properties without re-checking them. The Haskell service layer does not validate URLs after canonicalization succeeds because the contract guarantees the properties hold, and the prover has verified the guarantee. The contract defines the trust boundary. + +The same principle applies to short code generation: + +\begin{lstlisting}[language=Ada] +function Make_Short_Code (URL : Valid_URL; Secret : Secret_Key) + return Short_Code +with + Pre => Length (URL) >= 7, + Post => Length (Make_Short_Code'Result) = Short_Code_Length; +\end{lstlisting} + +The contract specifies fixed-length output, deterministic behavior, and no side effects. The precondition requires a \texttt{Valid\_URL}, which can only be constructed through successful canonicalization; the type system enforces the call ordering. These are architectural commitments encoded as proof obligations. + +% ============================================================================ +\section{Architecture Emerging from Constraints} +% ============================================================================ + +SPARK constraints directly influenced \texttt{hadlink}'s architecture in several ways. Each constraint, initially encountered as a limitation, became an architectural decision that improved the system. + +\subsection{Opaque Types as Proof-Driven Encapsulation} + +\texttt{Valid\_URL} and \texttt{Short\_Code} are declared as private types: + +\begin{lstlisting}[language=Ada] +type Valid_URL is private; +type Short_Code is private; +\end{lstlisting} + +This was not a style choice. The prover cannot reason about internal representation unless construction goes through a proven function. This enforces an invariant: \texttt{Valid\_URL} can only be created by successful canonicalization. The type system becomes an architectural boundary. Code that receives a \texttt{Valid\_URL} knows, by construction, that the URL has passed all validation checks. + +\subsection{Expression Functions for Proof Transparency} + +Query functions are written as expression functions (single-line definitions) because they are fully expanded during proof: + +\begin{lstlisting}[language=Ada] +function Is_HTTP_Or_HTTPS (URL : Valid_URL) return Boolean is + (Has_Valid_Scheme (To_String (URL))); +\end{lstlisting} + +A multi-line body function would require the prover to reason about function behavior indirectly, potentially requiring additional assumptions. The proof requirement drove the code structure toward simpler, more transparent definitions. + +\subsection{Ghost Lemma for Predicate Substitution} + +An attempt to use \texttt{Type\_Invariant} was blocked by SPARK RM 7.3.2(2) \cite{sparkrm}, which restricts type invariants in certain contexts. The workaround, a ghost lemma with two documented assumes for pure function determinism, confined all trust assumptions to a single location: + +\begin{lstlisting}[language=Ada] +pragma Assume (Has_Credentials (A) = Has_Credentials (B), + "Pure function determinism: A = B implies f(A) = f(B)"); +\end{lstlisting} + +These are the only two assumes in the entire codebase, both in a ghost procedure that generates no runtime code. The constraint shaped the proof strategy, which shaped the architecture: assumptions are explicit, localized, and documented. + +\subsection{Split Binaries from Proof Boundaries} + +The separation into shorten and redirect binaries was reinforced by SPARK. The redirect path needs no validation logic because URLs in the database are already canonical, which means the redirect binary has zero SPARK dependency. What began as a proof boundary naturally became an architectural boundary, and ultimately a deployment boundary. The component exposed to untrusted network traffic carries the smallest possible trusted computing base. + +% ============================================================================ +\section{Proof Results} +% ============================================================================ + +The verification results reflect the architectural choices described above. All 137 proof obligations are discharged automatically by the CVC5 SMT solver. + +\begin{table}[h] +\centering +\begin{tabular}{lr} +\toprule +Metric & Value \\ +\midrule +Total proof obligations & 137 \\ +Verified automatically (CVC5) & 137 (100\%) \\ +Explicit assumes & 2 (ghost lemma only) \\ +Assumes in business logic & 0 \\ +\bottomrule +\end{tabular} +\caption{Verification summary for \texttt{hadlink}'s SPARK core.} +\end{table} + +The proof obligations break down by type: range checks (31), overflow checks (30), preconditions (29), loop invariants (18), index checks (11), postconditions (9), and other checks including assertions, length, division, and initialization (9). All checks are solved in minimal SMT steps. The proofs are neither expensive nor fragile; they are natural consequences of contracts that accurately describe the code's behavior. When contracts match implementation cleanly, the prover's job is straightforward. + +% ============================================================================ +\section{Lessons Beyond SPARK} +% ============================================================================ + +The contract-first mindset transfers even without SPARK. Several principles emerge from the practice that apply to any engineering context. + +First, every function should declare its assumptions explicitly. Even without machine-checked contracts, documenting preconditions leads to cleaner APIs. Callers know what they must provide; implementations know what they can assume. Ambiguity at function boundaries is a source of bugs, and explicit assumptions reduce that ambiguity. + +Second, defining what a system will not do is as valuable as defining what it will do. \texttt{hadlink}'s non-goals (no analytics, no user accounts, no custom aliases) are documented and enforced. This practice, common in mature engineering organizations, prevents scope creep and communicates intent. The discipline of writing non-goals mirrors the discipline of writing preconditions: both constrain the system in ways that make reasoning easier. + +Third, if you cannot state a function's postcondition, you do not fully understand what it does. The act of writing postconditions forces clarity about behavior. What does this function guarantee? What can its caller rely on? These questions have answers whether or not you write them down, but writing them down reveals gaps in understanding. + +Finally, minimalism follows naturally from having to prove things about your code. Every additional feature is another proof obligation, another place where the contract must be specified and verified. This cost, even when only cognitive rather than computational, biases design toward simplicity. SPARK enforces these principles via the compiler \cite{sparkguidance}. Without SPARK, the same discipline can be applied through design reviews, documentation, and property-based testing. The compiler just makes it non-optional. + +% ============================================================================ +\section{Conclusion} +% ============================================================================ + +SPARK serves as both guardrail and mentor. The verification output is valuable: machine-checked guarantees that code satisfies its specification provide confidence that testing alone cannot. But the design discipline that emerges from writing contracts is also significant. For small infrastructure projects, formal methods need not be overhead. When applied early, they shape architecture in ways that reduce complexity and improve maintainability. + +The question for such projects is not ``can we afford to verify?'' but ``can we afford not to think this carefully?'' The contracts must be written regardless; SPARK simply ensures they are written precisely and checked mechanically. The architectural clarity that results is a welcome side effect of that precision. + +\section*{Availability} + +\texttt{hadlink} is open source and available at \url{https://github.com/Jbsco/hadlink}. + +\begin{thebibliography}{9} + +\bibitem{sparkrm} +AdaCore. +\textit{SPARK Reference Manual}. +\url{https://docs.adacore.com/spark2014-docs/html/lrm/} + +\bibitem{sparkguidance} +AdaCore and Thales. +\textit{Implementation Guidance for the Adoption of SPARK}, Release 1.2. +AdaCore, 2022. +\url{https://www.adacore.com/uploads/books/Spark-Guidance-1.2-web.pdf} + +\end{thebibliography} + +\end{document} diff --git a/docs/whitepapers/hadlink.pdf b/docs/whitepapers/hadlink.pdf new file mode 100644 index 0000000..49af6db Binary files /dev/null and b/docs/whitepapers/hadlink.pdf differ diff --git a/docs/whitepapers/hadlink.tex b/docs/whitepapers/hadlink.tex new file mode 100644 index 0000000..9495f67 --- /dev/null +++ b/docs/whitepapers/hadlink.tex @@ -0,0 +1,170 @@ +\documentclass[11pt,letterpaper]{article} +\usepackage[margin=1in]{geometry} +\usepackage{parskip} +\usepackage{hyperref} +\usepackage{listings} +\usepackage{xcolor} +\usepackage{booktabs} + +\lstset{ + basicstyle=\small\ttfamily, + keywordstyle=\color{blue!70!black}, + commentstyle=\color{gray}, + stringstyle=\color{red!60!black}, + showstringspaces=false, + breaklines=true, + frame=single, + xleftmargin=1em, + framexleftmargin=0.5em, +} + +\title{\texttt{hadlink}: A Minimal, High-Assurance URL Redirection Service} +\author{Jacob Seman} +\date{} + +\begin{document} +\maketitle + +\begin{abstract} +URL shorteners are deceptively small systems with disproportionate security consequences. Most implementations conflate policy and mechanism, trust input too broadly, and are difficult to reason about. \texttt{hadlink} is a URL redirection service designed for infrastructure use cases (CI/CD pipelines, QR codes, SMS notifications) where deterministic behavior, security, and auditability matter more than feature breadth. Its core validation and encoding logic is formally verified using SPARK Ada, while the service layer is composed in Haskell with conservative dependencies. This paper describes the system's design philosophy, assurance model, and deployment approach. +\end{abstract} + +% ============================================================================ +\section{Problem Statement} +% ============================================================================ + +Any service that accepts arbitrary URLs and redirects traffic to them becomes, in effect, an open relay. URL shorteners are frequent abuse targets for spam campaigns, phishing attacks, and malware distribution. The opacity of the short code, hiding the destination until the redirect occurs, is precisely what makes them useful and precisely what makes them dangerous. Despite this, most shorteners are deployed casually, with minimal validation and no formal reasoning about their behavior. + +Most URL shortener implementations share common weaknesses. They conflate policy and mechanism, mixing validation logic with routing logic with storage logic in ways that make reasoning about behavior difficult. They trust input too broadly, accepting URLs that point to private network addresses, contain embedded credentials, or use non-HTTP schemes. They offer no formal specification of what the system guarantees, leaving behavior to vary unpredictably with input. + +The problem is small enough to be tractable for formal methods. A URL shortener's core logic (validating input, generating short codes, storing mappings, and performing redirects) can be specified precisely and verified completely. The effort is justified because the consequences of getting it wrong extend beyond the service itself to every system that trusts its output. + +% ============================================================================ +\section{Design Goals and Non-Goals} +% ============================================================================ + +\subsection{Goals} + +\texttt{hadlink} targets infrastructure use cases where predictability matters more than features. Four goals guide the design. First, deterministic behavior: the same input URL always produces the same short code, enabling idempotent operations and predictable caching. Second, a minimal trusted computing base: the verified core contains no I/O, networking, storage, or concurrency, limiting the attack surface to well-understood components. Third, explicit failure modes: all errors are enumerated, and the system never fails silently or returns ambiguous results. Fourth, constrained deployability: a single binary with SQLite storage runs on minimal hardware with no external service dependencies. + +\subsection{Non-Goals} + +Equally important are the things \texttt{hadlink} will not do. It provides no marketing analytics or click tracking. It has no user accounts, dashboards, or authentication layer. It does not support custom aliases, vanity URLs, or dynamic policy engines. It performs no JavaScript redirects, link previews, or interstitial pages. It does not aim for feature parity with SaaS shorteners like Bitly or TinyURL. + +These are conscious trade-offs, not omissions. Each excluded feature would add complexity, expand the attack surface, or conflict with the determinism requirement. Non-goals are documented in the repository and enforced in the contribution policy: pull requests that conflict with stated non-goals are closed with explanation, not negotiated. + +% ============================================================================ +\section{Architecture} +% ============================================================================ + +\texttt{hadlink} uses a two-layer design with intentional separation between verified core logic and service composition. + +\subsection{SPARK Core} + +The formally verified core handles URL canonicalization and short code generation. Canonicalization validates the URL scheme (HTTP or HTTPS only), rejects URLs pointing to private addresses (RFC 1918, RFC 4193, link-local), and detects embedded credentials. Short code generation uses HMAC-SHA256 via SPARKNaCl, producing deterministic 8-character Base62 codes. + +The SPARK core contains no I/O, networking, storage, concurrency, or configuration parsing. It is pure computation with explicit preconditions and postconditions \cite{sparkguidance}. All 137 proof obligations are verified automatically by the CVC5 SMT solver. + +\subsection{Haskell Service Layer} + +The service layer composes the system from conservative dependencies. HTTP handling uses Warp, chosen for its minimal API surface and proven reliability. Storage relies on SQLite in WAL mode for its simplicity and reliability. Rate limiting, structured logging, and proof-of-work validation are implemented in Haskell and tested via Hedgehog property tests. + +The service layer trusts the SPARK core's postconditions: if canonicalization succeeds, the URL satisfies all security properties. This trust boundary is explicit and documented. + +\subsection{Foreign Function Interface} + +The Foreign Function Interface (FFI) between layers is minimal and frozen at API version 1. Three C functions are exported: \texttt{hadlink\_canonicalize}, \texttt{hadlink\_make\_short\_code}, and \texttt{hadlink\_api\_version}. The FFI marshaling code is explicitly outside SPARK verification (\texttt{pragma SPARK\_Mode Off}) and is tested separately. + +A freeze test in the test suite ensures the interface does not change without a corresponding version bump. The FFI is thin by design: data crosses the boundary as C strings with explicit length parameters, and all memory is caller-allocated. + +\subsection{Split Binaries} + +Two separate executables serve different trust profiles. \texttt{hadlink-redirect} handles the read path, looking up short codes and returning redirects. It is fast and stateless, linking no SPARK code and carrying no dependency on \texttt{libHadlink\_Core.so}. This binary is designed to be exposed to the public network. + +\texttt{hadlink-shorten} handles the write path: it validates URLs, generates short codes, and stores mappings. It includes the SPARK FFI, rate limiting, and proof-of-work validation. It is designed to be restricted to internal networks or authenticated access. + +This separation is least-privilege at the binary level. The component exposed to untrusted traffic has the smallest possible attack surface. + +\subsection{Storage} + +SQLite in WAL mode provides the storage layer. The schema contains three columns: the short code serving as primary key, the canonical URL, and a creation timestamp. The write path is append-only, with no update or delete operations supported. + +\texttt{INSERT OR IGNORE} provides idempotent creation. Because short codes are deterministic (same URL always produces same code), duplicate requests are harmless: they either insert a new row or silently succeed when the row already exists. The redirect service opens the database read-only. + +% ============================================================================ +\section{Formal Assurance} +% ============================================================================ + +The SPARK core provides machine-checked guarantees about the system's behavior. Every stored URL is proven to have a valid HTTP or HTTPS scheme, contain no embedded credentials, and point to no private network address. Short codes are guaranteed to be exactly 8 Base62 characters. All array accesses are proven in-bounds, and the encoding logic is verified free of integer overflow. + +\begin{table}[h] +\centering +\begin{tabular}{lr} +\toprule +Check type & Count \\ +\midrule +Range checks & 31 \\ +Overflow checks & 30 \\ +Preconditions & 29 \\ +Loop invariants & 18 \\ +Index checks & 11 \\ +Postconditions & 9 \\ +Other (assert, length, division, init) & 9 \\ +\midrule +Total & 137 \\ +\bottomrule +\end{tabular} +\caption{Proof obligation breakdown by check type.} +\end{table} + +The verification boundary is explicit about what is not proven. FFI marshaling is outside SPARK verification and tested separately. The Haskell service layer is property-tested via Hedgehog but not formally verified. SQLite is a trusted dependency. Network-level properties (TLS termination, DNS resolution) are outside the system's scope. + +Assumptions are confined and documented. The codebase contains exactly two \texttt{pragma Assume} statements, both in a ghost lemma that generates no runtime code. Both document pure function determinism: if two inputs are equal, their outputs are equal. There are zero assumes in business logic. + +The project references DO-278A (Software Integrity Level 3) as an architectural guide for separation of concerns and evidence requirements. It is not certified; this is a single-developer project without independent verification resources. The formal methods provide confidence, not certification. + +% ============================================================================ +\section{Deployment} +% ============================================================================ + +\texttt{hadlink} supports three deployment methods. Docker images use pre-built binaries from GitHub Releases or can be built from source. Systemd unit files provide direct installation with security hardening. An Arch Linux AUR package (\texttt{hadlink-bin}) offers distribution-native installation. + +The systemd configuration applies defense-in-depth hardening: \texttt{NoNewPrivileges}, \texttt{ProtectSystem=strict}, \texttt{ProtectHome}, \texttt{PrivateTmp}, and \texttt{MemoryDenyWriteExecute}. Resource limits are conservative: 128MB for the shorten service, 64MB for redirect. Both services restart on failure with a 5-second delay. + +Configuration follows a minimalist approach, using environment variables only with no configuration file parser to introduce complexity or parsing vulnerabilities. Secret management uses systemd's \texttt{EnvironmentFile} directive, keeping secrets out of unit files and command lines. + +The redirect service is stateless and recovers instantly from restarts. The shorten service holds no persistent in-memory state; its STM-based rate limiter rebuilds on startup. Pre-built binaries are available from GitHub Releases, so deployment requires no build toolchain. Operators can run \texttt{hadlink} without installing GHC, GNAT, or any development dependencies. + +% ============================================================================ +\section{Limitations and Future Work} +% ============================================================================ + +\texttt{hadlink} has intentional limitations that preserve its design properties. SQLite's scaling envelope is sufficient for infrastructure use cases but not for high-volume marketing workloads processing millions of redirects per second. There is no built-in abuse detection; rate limiting and proof-of-work mitigate automated abuse but do not detect malicious destination URLs. The system is single-node only, with no replication or distributed deployment. URLs cannot expire or be deleted; the append-only design ensures that short codes are permanent and deterministic. + +These are conscious trade-offs. SQLite's simplicity eliminates an entire class of distributed systems failures. The absence of abuse detection keeps the system policy-neutral, allowing operators to layer their own detection upstream. Single-node deployment means no consensus protocol, no split-brain scenarios, no coordination overhead. Permanent URLs mean short codes can be printed on physical media without expiration concerns. + +Potential future work includes an LMDB backend for higher read throughput, native TLS termination (currently the system relies on a reverse proxy), and a Prometheus metrics endpoint for operational visibility. None of these would change the core assurance model. + +% ============================================================================ +\section{Conclusion} +% ============================================================================ + +\texttt{hadlink} demonstrates that formal methods are tractable for small infrastructure services. The system prioritizes correctness over features and treats simplicity as a security primitive. By confining verified logic to a pure computational core and composing the service layer from conservative dependencies, it achieves high assurance without the overhead typically associated with formal verification. + +The approach (SPARK core with explicit contracts, thin FFI boundary, Haskell composition layer) is applicable to other services with similar trust requirements: authentication tokens, configuration validators, cryptographic utilities, and anywhere a small component has disproportionate security impact. The question for such systems is not whether formal methods are worth the effort, but whether the alternative, trusting unverified code in critical paths, is acceptable. + +\section*{Availability} + +\texttt{hadlink} is open source and available at \url{https://github.com/Jbsco/hadlink}. + +\begin{thebibliography}{9} + +\bibitem{sparkguidance} +AdaCore and Thales. +\textit{Implementation Guidance for the Adoption of SPARK}, Release 1.2. +AdaCore, 2022. +\url{https://www.adacore.com/uploads/books/Spark-Guidance-1.2-web.pdf} + +\end{thebibliography} + +\end{document} diff --git a/docs/whitepapers/sprint-projects.pdf b/docs/whitepapers/sprint-projects.pdf new file mode 100644 index 0000000..9246ffb Binary files /dev/null and b/docs/whitepapers/sprint-projects.pdf differ diff --git a/docs/whitepapers/sprint-projects.tex b/docs/whitepapers/sprint-projects.tex new file mode 100644 index 0000000..b1c13f7 --- /dev/null +++ b/docs/whitepapers/sprint-projects.tex @@ -0,0 +1,98 @@ +\documentclass[11pt,letterpaper]{article} +\usepackage[margin=1in]{geometry} +\usepackage{parskip} +\usepackage{hyperref} +\usepackage{enumitem} + +\title{From Coursework to Craft:\\Single-Sprint Projects as Engineering Practice} +\author{Jacob Seman} +\date{} + +\begin{document} +\maketitle + +\begin{abstract} +Undergraduate engineering coursework builds breadth and teaches students to finish under externally imposed constraints. These are necessary skills, but they are not sufficient preparation for professional practice. Short-timeline personal projects, constrained to one or two weeks, complement coursework by training scope discipline, invariant-driven design, and the judgment to stop. This paper compares both modes of learning and argues that single-sprint projects are effective deliberate practice for engineering skills that coursework alone does not emphasize. Programs that integrate frequent project work alongside traditional coursework better prepare students for the realities of professional engineering. +\end{abstract} + +% ============================================================================ +\section{Introduction} +% ============================================================================ + +Not all engineering programs are structured the same way. Some are built primarily around homework sets and exams, with projects appearing only as semester-long capstones. Others intersperse shorter, frequent projects on two- to four-week timelines alongside traditional coursework. The difference matters. In programs that provision sprint-like projects throughout the curriculum, students practice scoping, designing, and delivering complete systems multiple times per semester. In programs that do not, students may graduate having completed only one or two open-ended projects in four years. + +Both models build foundational knowledge. But programs that include frequent short projects better approximate the rhythm of professional engineering, where the unit of work is not a problem set or an exam but a bounded deliverable with real trade-offs. Students in these programs learn earlier that finishing is not the same as completing, and that deciding what to leave out is as important as deciding what to include. + +This paper argues that single-sprint personal projects, constrained to one or two weeks with a self-imposed scope and a production-quality target, complement both models of coursework. For students in project-heavy programs, they reinforce and extend skills already being developed. For students in traditional programs, they fill a gap that homework and exams cannot address. In either case, they train ownership, architectural judgment, and restraint in ways that externally defined coursework does not. + +% ============================================================================ +\section{What Coursework Does Well} +% ============================================================================ + +Electrical and computer engineering programs, in particular, expose students to a demanding breadth of work. In any given semester a student may be running multiple parallel efforts across digital design, analog circuits, embedded systems, and software, each with its own tools, constraints, and deadlines. This forces rapid context-switching and builds a broad technical surface area that is difficult to acquire any other way. Grades incentivize finishing, and finishing under someone else's constraints is not trivial. Fixed deadlines, shifting requirements, and collaborative dynamics all mirror aspects of professional work. + +Programs that provision shorter, frequent projects within the syllabus go further. When a two- to four-week project appears alongside homework and exams, students practice a different set of skills: time and scope management against competing obligations, design around fixed requirements with real trade-offs, and documentation of friction points and future work. These programs produce graduates who have already experienced the cycle of scoping, building, and delivering multiple times before entering the workforce. The project cadence itself is a form of training. + +Programs built exclusively around homework, exams, and a single capstone do not offer this repetition. Students in these programs are often technically strong but have limited practice making the kinds of decisions that define professional work: what to build, what to cut, and when a system is done. The grade incentive rewards completion and breadth, which are necessary but not sufficient. The skills that distinguish a competent engineer from a mature one, scope judgment, architectural restraint, and the confidence to leave things out, require repeated practice that traditional coursework alone does not provide. + +% ============================================================================ +\section{What Coursework Does Not Emphasize} +% ============================================================================ + +Programs that include frequent projects develop these skills partially, but even in those programs the scope is externally defined. The rubric sets the floor, the deadline sets the ceiling, and the student optimizes within that frame. Three skills in particular are difficult to train under externally imposed constraints. + +\subsection{Scope Discipline} + +In coursework, scope creep is expected. Requirements change mid-semester, features get added to satisfy rubric items, and cutting functionality feels like losing points. The incentive structure rewards inclusion: more features, more demonstrations, more coverage. Even in project-heavy programs, the scope is given, not chosen. + +In professional practice, the opposite is often true. Most engineering value comes from what you choose not to build. A self-directed project forces this directly. There is no rubric to optimize for, no teaching assistant to ask for an extension. You must decide what matters, what does not, and then commit to the boundary. This is scope discipline, and it is difficult to practice when someone else defines the scope for you. + +\subsection{Invariant-Driven Design} + +Course projects tend to emphasize outputs: demonstrations, reports, and the happy path working on presentation day. Sprint projects reward a different approach, defining invariants early and designing around failure modes. When you have one week, you cannot afford to discover your core assumptions were wrong on day five. You are forced to state what must always be true and build outward from there. + +This extends naturally to the concept of design by non-goals: explicitly documenting what the system will never do and enforcing those boundaries in practice. Non-goal documentation is uncommon in coursework but standard in mature engineering organizations, where it prevents scope drift and communicates intent to future maintainers. + +\subsection{Taste and Restraint} + +You cannot brute-force a one-week project with complexity. You must choose conservative tools, reject clever abstractions, and bias toward debuggability over expressiveness. This is professional taste forming, the development of judgment about what belongs in a system and what does not. It is difficult to practice in a semester-long project where complexity can always be deferred to next week or absorbed by a teammate. + +% ============================================================================ +\section{Single-Sprint Projects as Deliberate Practice} +% ============================================================================ + +The format is simple: one to two weeks, a self-imposed scope, and a production-quality target. The project must be something you can define in a single sentence, small enough to be tractable but real enough to require genuine design decisions. The constraint is the point, and there is no grade safety net or partial credit to fall back on. Every decision reflects directly on you, and design trade-offs are permanent. + +In academic settings, a ``sprint'' usually means a burst of effort before a deadline. In professional practice, a sprint is a bounded commitment with explicit deliverables and explicit cuts. Single-sprint personal projects practice the latter. They force you to decide what ships and what does not before the work begins, then hold yourself to that boundary as the work reveals its actual complexity. + +This is also where time management and expectation management are learned organically. There is no project manager but yourself, responsible for estimating, prioritizing, cutting, and shipping. The feedback loop is immediate: if you scoped poorly, you either ship something incomplete or you learn to scope better next time. Both outcomes are instructive. + +% ============================================================================ +\section{A Concrete Example} +% ============================================================================ + +In a recent single-sprint project, I constrained myself to a ten-day timeline and a sharply defined problem: a URL redirection service with formally verified core logic. The first commit was on January 22, 2026; version 1.0.0 shipped on February 1. The timeline forced decisions that a longer project would have deferred. Non-goals were documented before goals: no analytics, no user accounts, no custom aliases, no web interface, no click tracking. These were not features cut for time. They were excluded by design and enforced in the contribution policy. + +The central design invariant, that all stored URLs are canonicalized and satisfy four security properties, was established on day one and guided every subsequent architectural decision. The validated core was written in SPARK Ada with formal proof obligations. The service layer was composed in Haskell using conservative dependencies: SQLite for storage, Warp for HTTP. A phased internal roadmap, from v0.1.0 through v0.5.0 to v1.0.0, provided structure within the sprint and made scope visible at each stage. + +The result was a small but production-ready system with 137 verified proof obligations rather than an expanding prototype. The project succeeded not because the timeline was generous, but because the scope was honest. Every feature that shipped was intentional, and every feature that was excluded was documented. + +% ============================================================================ +\section{Lessons and Advice} +% ============================================================================ + +For students and early-career engineers looking to build this practice, the approach is straightforward. Pick a problem you can define in one sentence. Write your non-goals before your goals. Set a hard deadline and do not move it. Ship something real, even if small. Treat the constraint as the feature, not the limitation. + +The temptation will be to expand scope once the work feels productive. Resist it. The discipline of stopping, of declaring a system complete while there are still obvious things you could add, is the skill being practiced. A finished project with clear boundaries teaches more than an ambitious prototype that never ships. + +The broader point is that the habit of scoping, cutting, and shipping builds a skill set that coursework alone does not develop. Neither mode of learning is sufficient on its own. Together, they approximate the reality of professional engineering, where the ability to decide what to build matters as much as the ability to build it. + +% ============================================================================ +\section{Conclusion} +% ============================================================================ + +Coursework and single-sprint projects are complementary forms of engineering practice. Programs that already integrate frequent short projects into the syllabus have a measurable advantage: their students arrive at the workforce having practiced the cycle of scoping, building, and shipping multiple times. Sprint projects extend this further by removing the external scaffolding entirely, training judgment, ownership, and restraint in their purest form. For students in traditional, exam-heavy programs, self-directed sprint projects fill a critical gap that no amount of problem sets can address. + +These are the skills that distinguish an engineer who can build from one who can decide what to build. They are best developed through repetition, through the habit of picking a small problem, defining its boundaries honestly, and finishing it well. The earlier that habit forms, whether through program structure or personal initiative, the stronger the engineer it produces. + +\end{document}