diff --git a/compiler/spec/0001-Introduction.md b/compiler/spec/0001-Introduction.md
index cf25272..c94e3c1 100644
--- a/compiler/spec/0001-Introduction.md
+++ b/compiler/spec/0001-Introduction.md
@@ -1,33 +1,28 @@
 # Introduction
 
-- [Completeness](#completeness)
-- [Core Principles](#core-principles)
+Osprey is a functional programming language designed for safety, performance, and expressiveness.
 
-Osprey is a modern functional programming language designed for elegance, safety, and performance. It emphasizes:
+## Core Features
 
-- **Named arguments** for multi-parameter functions to improve readability
-- **Strong type inference** to reduce boilerplate while maintaining safety
-- **String interpolation** for convenient text formatting
-- **Pattern matching** for elegant conditional logic
-- **Immutable-by-default** variables with explicit mutability
-- **Fast HTTP servers and clients** with built-in streaming support
-- **WebSocket support** for real-time two-way communication
+- Named arguments for multi-parameter functions
+- Hindley-Milner type inference with strong static typing
+- Pattern matching for all conditional logic
+- Immutable-by-default with explicit mutability
+- Algebraic effects with compile-time safety
+- Result types for all error cases (no exceptions or panics)
+- Built-in HTTP/WebSocket support with streaming
+- Lightweight fiber-based concurrency
 
-## Completeness
+## Design Principles
 
-**Note**: The Osprey language and compiler are under active development. This specification represents design goals and planned features. The spec is the authoritative source for syntax and behavior.
+- **Safety**: Make illegal states unrepresentable through static verification
+- **Simplicity**: One idiomatic way to accomplish each task
+- **Performance**: LLVM compilation with Rust interop for performance-critical code
+- **Functional**: Referential transparency, immutable data structures, pure functions
+- **Type Safety**: Strong static typing with Hindley-Milner inference; `any` type requires explicit declaration
+- **No Exceptions**: All error cases return Result types, enforced at compile time
+- **ML Heritage**: Syntax and semantics inspired by ML family languages
 
-## Core Principles
+## Development Status
 
-- Elegance (simplicity, ergonomics, efficiency), safety (fewer footguns, security at every level), performance (uses the most efficient approach and allows the use of Rust interop for extreme performance)
-- No more than 1 way to do anything
-- ML style syntax by default
-- Make illegal states unrepresentable. There are no exceptions or panics. Anything than can result in an error state returns a result object
-- Referential transparency
-- Simplicity
-- Interopability with Rust for high performance workloads
-- Interopability with Haskell (future) for fundamental correctness
-- Static/strong typing. Nothing should be "any" unless EXPLICITLY declared as any
-- Minimal ceremony. No main function necessary for example.
-- **Fast HTTP performance** as a core design principle
-- **Streaming by default** for large responses to prevent memory issues
\ No newline at end of file
+This specification is the authoritative source for Osprey syntax and behavior. The language and compiler are under active development; implementation status is noted where relevant.
\ No newline at end of file
diff --git a/compiler/spec/0002-LexicalStructure.md b/compiler/spec/0002-LexicalStructure.md
index 03abedd..d967d13 100644
--- a/compiler/spec/0002-LexicalStructure.md
+++ b/compiler/spec/0002-LexicalStructure.md
@@ -79,43 +79,30 @@ let pair = [x, y]  // Fixed size: 2 elements
 
 ### Arithmetic Operators
 
-All arithmetic operators are type-preserving and return `Result` types to handle errors (overflow, underflow, division by zero).
+All arithmetic operators return `Result` types to handle overflow, underflow, and division by zero.
 
-**Integer Arithmetic:**
+**Integer Operations:**
 - `+` Addition: `(int, int) -> Result<int, MathError>`
 - `-` Subtraction: `(int, int) -> Result<int, MathError>`
 - `*` Multiplication: `(int, int) -> Result<int, MathError>`
-- `/` Division: `(int, int) -> Result<float, MathError>` - Auto-promotes to float (10 / 3 = 3.333...)
-- `%` Modulo: `(int, int) -> Result<int, MathError>` - Returns remainder (10 % 3 = 1)
+- `/` Division: `(int, int) -> Result<float, MathError>` — always returns float
+- `%` Modulo: `(int, int) -> Result<int, MathError>`
 
-**Floating-Point Arithmetic:**
-- `+` Addition: `(float, float) -> Result<float, MathError>`
-- `-` Subtraction: `(float, float) -> Result<float, MathError>`
-- `*` Multiplication: `(float, float) -> Result<float, MathError>`
-- `/` Division: `(float, float) -> Result<float, MathError>` - IEEE 754 division (10.0 / 3.0 = 3.333...)
-- `%` Modulo: `(float, float) -> Result<float, MathError>` - IEEE 754 remainder
+**Floating-Point Operations:**
+- `+`, `-`, `*`, `/`, `%`: `(float, float) -> Result<float, MathError>`
 
 **Type Safety:**
-- No automatic type promotion: cannot mix int and float in operations
-- Use `toFloat(int)` to convert int to float: `toFloat(10) / 3.0`
-- Use `toInt(float)` to truncate float to int: `toInt(3.7) = 3`
+- No automatic type promotion between int and float
+- Use `toFloat(int)` and `toInt(float)` for explicit conversion
+- Division `/` always returns float, even for integer operands
 
 **Examples:**
 ```osprey
-// Integer arithmetic
-let sum = 5 + 3           // Result<int, MathError> - Success(8)
-let quotient = 10 / 3     // Result<float, MathError> - Success(3.333...) - Auto-promotes to float!
-let remainder = 10 % 3    // Result<int, MathError> - Success(1)
+let sum = 5 + 3           // Result<int, MathError>
+let quotient = 10 / 3     // Result<float, MathError> - returns 3.333...
+let remainder = 10 % 3    // Result<int, MathError> - returns 1
 
-// Floating-point arithmetic
-let precise = 10.0 / 3.0  // Result<float, MathError> - Success(3.333...)
-let area = 3.14 * 2.5     // Result<float, MathError> - Success(7.85)
-
-// Division always returns float
-let intDiv = 10 / 2       // Result<float, MathError> - Success(5.0) - Float result!
-let mixedDiv = 10 / 3     // Result<float, MathError> - Success(3.333...)
-
-// Error cases
+let precise = 10.0 / 3.0  // Result<float, MathError>
 let divZero = 10 / 0      // Result<float, MathError> - Error(DivisionByZero)
 ```
 
diff --git a/compiler/spec/0003-Syntax.md b/compiler/spec/0003-Syntax.md
index eb99c92..5d162ab 100644
--- a/compiler/spec/0003-Syntax.md
+++ b/compiler/spec/0003-Syntax.md
@@ -249,43 +249,30 @@ let max = match a > b {
 }
 ```
 
-#### List Access (Safe)
+#### List Access
+
 ```
 list_access := expression '[' INT ']'  // Returns Result<T, IndexError>
 ```
 
-🚨 **CRITICAL SAFETY GUARANTEE**: List access **ALWAYS** returns `Result<T, IndexError>` - **NO PANICS, NO NULLS, NO EXCEPTIONS**
+List access always returns `Result<T, IndexError>` for bounds safety and must be handled with pattern matching:
 
-**MANDATORY PATTERN MATCHING REQUIRED:**
 ```osprey
 let numbers = [1, 2, 3, 4]
 
-// ✅ CORRECT: Pattern matching required
-let firstResult = numbers[0]  // Returns Result<Int, IndexError>
+let firstResult = numbers[0]  // Result<int, IndexError>
 match firstResult {
     Success { value } => print("First: ${value}")
-    Error { message } => print("Index out of bounds: ${message}")
+    Error { message } => print("Index error: ${message}")
 }
 
-// ✅ CORRECT: Inline pattern matching
+// Inline pattern matching
 let second = match numbers[1] {
     Success { value } => value
-    Error { _ } => -1  // Default value for out-of-bounds
-}
-
-// ✅ CORRECT: Bounds-safe iteration
-let commands = ["echo hello", "echo world"]
-match commands[0] {
-    Success { value } => {
-        print("Executing: ${value}")
-        spawnProcess(value)
-    }
-    Error { message } => print("No command at index 0: ${message}")
+    Error { _ } => -1
 }
 ```
 
-**FUNDAMENTAL SAFETY PRINCIPLE**: Array access can fail (index out of bounds), therefore it MUST return Result types to enforce explicit error handling and prevent runtime crashes.
-
 #### Field Access
 
 Field access uses dot notation to access fields of record types:
@@ -311,54 +298,33 @@ print("Age: ${person.age}")
 sendEmail(to: person.name, subject: "Hello")
 ```
 
-#### Field Access Rules and Restrictions
+#### Field Access Rules
 
-**✅ ALLOWED - Field Access on Record Types:**
-```osprey
-type User = { id: Int, name: String, email: String }
-let user = User { id: 1, name: "Alice", email: "alice@example.com" }
-
-let userId = user.id          // Valid: direct field access
-let userName = user.name      // Valid: direct field access
-let userEmail = user.email    // Valid: direct field access
-```
+Field access is allowed on record types:
 
-**❌ FORBIDDEN - Field Access on `any` Types:**
 ```osprey
-fn processAnyValue(value: any) -> String = {
-    // ERROR: Cannot access fields on 'any' type
-    let result = value.name   // Compilation error
-    return result
-}
-
-// CORRECT: Use pattern matching for 'any' types
-fn processAnyValue(value: any) -> String = match value {
-    person: { name } => person.name        // Extract field via pattern matching
-    user: User { name } => name           // Type-specific pattern matching
-    _ => "unknown"
-}
+type User = { id: int, name: string }
+let user = User { id: 1, name: "Alice" }
+let userId = user.id          // Valid
+let userName = user.name      // Valid
 ```
 
-**❌ FORBIDDEN - Field Access on Result Types:**
-```osprey
-type Person = { 
-    name: String
-} where validatePerson
+Field access requires pattern matching for:
+- **`any` types**: Extract fields through structural patterns
+- **Result types**: Unwrap Result before accessing fields
+- **Union types**: Match variant before accessing fields
 
-fn validatePerson(person: Person) -> Result<Person, String> = match person.name {
-    "" => Error("Name cannot be empty")
-    _ => Success(person)
+```osprey
+// any type - use pattern matching
+fn processAny(value: any) -> string = match value {
+    person: { name } => person.name
+    _ => "unknown"
 }
 
-let personResult = Person { name: "Alice" }  // Returns Result<Person, String>
-
-// ERROR: Cannot access field on Result type
-let name = personResult.name   // Compilation error
-
-// CORRECT: Use pattern matching on Result types
+// Result type - unwrap first
 match personResult {
-    Ok { value } => print("Name: ${value.name}")    // Access field after unwrapping
-    Err { error } => print("Construction failed: ${error}")
+    Success { value } => print("Name: ${value.name}")
+    Error { message } => print("Error: ${message}")
 }
 ```
 
@@ -569,62 +535,7 @@ let wrong: int = {
 }
 ```
 
-#### Performance Characteristics
-
-Block expressions are zero-cost abstractions:
-- **Compile-time scoping**: All variable scoping resolved at compile time
-- **No runtime overhead**: Blocks compile to sequential instructions
-- **Stack allocation**: Local variables allocated on the stack
-- **Optimized away**: Simple blocks with no local variables are optimized away
-
-#### Best Practices
-
-**Use block expressions when:**
-- You need local variables for complex calculations
-- Breaking down complex expressions into readable steps
-- Implementing complex match arm logic
-- Creating temporary scopes to avoid variable name conflicts
-
-**Avoid block expressions when:**
-- A simple expression would suffice
-- The block only contains a single expression
-- Creating unnecessary nesting levels
-
-**Good Examples:**
-```osprey
-// Good: Complex calculation with intermediate steps
-let result = {
-    let base = getUserInput()
-    let squared = base * base
-    let doubled = squared * 2
-    squared + doubled
-}
-
-// Good: Complex match logic
-let response = match request.method {
-    POST => {
-        let body = parseBody(request.body)
-        let validated = validateData(body)
-        processCreation(validated)
-    }
-    _ => "Method not allowed"
-}
-```
-
-**Bad Examples:**
-```osprey
-// Bad: Unnecessary block for simple expression
-let bad = {
-    42
-}
-// Better: let bad = 42
-
-// Bad: Single operation doesn't need block
-let also_bad = {
-    x + y
-}
-// Better: let also_bad = x + y
-```
+Block expressions are zero-cost abstractions: scoping is resolved at compile time, and simple blocks are optimized away. See [Block Expressions](0008-BlockExpressions.md) for complete details on semantics and usage patterns.
 
 ### Match Expressions
 
diff --git a/compiler/spec/0004-TypeSystem.md b/compiler/spec/0004-TypeSystem.md
index d24fd4d..2092c96 100644
--- a/compiler/spec/0004-TypeSystem.md
+++ b/compiler/spec/0004-TypeSystem.md
@@ -2,38 +2,8 @@
 
 - [Hindley-Milner Type Inference](#hindley-milner-type-inference)
 - [Built-in Types](#built-in-types)
-  - [Function Types](#function-types)
-  - [Record Types](#record-types)
-  - [Collection Types (List and Map)](#collection-types-list-and-map)
-- [Built-in Error Types](#built-in-error-types)
-- [Hindley-Milner Type Inference](#hindley-milner-type-inference-1)
-  - [Hindley-Milner Function Inference](#hindley-milner-function-inference)
-  - [Constraint-Based Type Inference](#constraint-based-type-inference)
-  - [Hindley-Milner Implementation Examples](#hindley-milner-implementation-examples)
-  - [Hindley-Milner Benefits](#hindley-milner-benefits)
-  - [Record Type Structural Equivalence](#record-type-structural-equivalence)
-  - [Polymorphic Type Variables vs Any Type](#polymorphic-type-variables-vs-any-type)
-  - [Hindley-Milner Constraint Resolution](#hindley-milner-constraint-resolution)
-- [Type Safety and Explicit Typing](#type-safety-and-explicit-typing)
-  - [Mandatory Type Safety](#mandatory-type-safety)
-- [Any Type Handling and Pattern Matching Requirement](#any-type-handling-and-pattern-matching-requirement)
-  - [Forbidden Operations on `any` Types](#forbidden-operations-on-any-types)
-  - [Legal Operations on `any` Types](#legal-operations-on-any-types)
-  - [Pattern Matching Requirement](#pattern-matching-requirement)
-  - [Direct Access Compilation Errors](#direct-access-compilation-errors)
-  - [Function Return Type Handling](#function-return-type-handling)
-  - [Type Annotation Pattern Syntax](#type-annotation-pattern-syntax)
-  - [Compilation Error Messages](#compilation-error-messages)
-  - [Exhaustiveness Checking for Any Types](#exhaustiveness-checking-for-any-types)
-  - [Default Wildcard Behavior for Any Types](#default-wildcard-behavior-for-any-types)
-  - [Type Constraint Checking](#type-constraint-checking)
-  - [Context-Aware Type Validation](#context-aware-type-validation)
-  - [Compilation Errors for Impossible Types](#compilation-errors-for-impossible-types)
-  - [Performance and Safety Characteristics](#performance-and-safety-characteristics)
-  - [Type Annotation Requirements](#type-annotation-requirements)
-  - [Compilation Errors for Type Ambiguity](#compilation-errors-for-type-ambiguity)
-  - [Error Handling Requirements](#error-handling-requirements)
-  - [Type-Level Validation](#type-level-validation)
+- [Type Safety](#type-safety)
+- [Any Type Handling](#any-type-handling)
 - [Type Compatibility](#type-compatibility)
 
 ## Hindley-Milner Type Inference
@@ -382,50 +352,29 @@ let result = ValidatedPerson { name: "Bob", age: 25, email: "bob@example.com" }
 
 **Field Access Rules:**
 
-**🔥 CRITICAL SPECIFICATION: FIELD ACCESS IS STRICTLY BY NAME ONLY**
+Record field access is strictly by name only. Field ordering is not significant and must not be relied upon by the compiler implementation.
 
-**ABSOLUTE REQUIREMENT**: Record field access is **EXCLUSIVELY BY NAME**. Field ordering, positioning, or indexing is **COMPLETELY FORBIDDEN** and must **NEVER** be relied upon by the compiler implementation.
-
-**✅ ALLOWED - Field Access on Record Types (BY NAME ONLY):**
 ```osprey
 type User = { id: int, name: string, email: string }
 let user = User { id: 1, name: "Alice", email: "alice@example.com" }
 
-let userId = user.id          // ✅ VALID: direct field access BY NAME
-let userName = user.name      // ✅ VALID: direct field access BY NAME  
-let userEmail = user.email    // ✅ VALID: direct field access BY NAME
+// Field access by name
+let userId = user.id
+let userName = user.name
 
-// Field order during construction is IRRELEVANT
-let user2 = User { 
-    email: "bob@example.com",  // Different order - PERFECTLY VALID
-    name: "Bob",               // Field position does NOT matter
-    id: 2                      // Only field NAMES matter
+// Field order during construction is irrelevant
+let user2 = User {
+    email: "bob@example.com",
+    name: "Bob",
+    id: 2
 }
-let bobName = user2.name      // ✅ VALID: name-based access works regardless of declaration order
-```
-
-**❌ ABSOLUTELY FORBIDDEN - Positional or Indexed Access:**
-```osprey
-// NEVER ALLOWED - These are COMPILATION ERRORS
-let value1 = user[0]          // ❌ FORBIDDEN: No indexed access  
-let value2 = user.fields[1]   // ❌ FORBIDDEN: No positional access
-let value3 = getFieldAt(user, 0)  // ❌ FORBIDDEN: No position-based access
-
-// COMPILER IMPLEMENTATION MUST NEVER:
-// - Rely on field declaration order for LLVM struct generation
-// - Use field positioning for type unification
-// - Access fields by index in any internal operation
-// - Generate code that depends on field ordering
 ```
 
-**🔥 COMPILER IMPLEMENTATION REQUIREMENT:**
-The Osprey compiler **MUST** implement field access using **FIELD NAME LOOKUP ONLY**:
-- ✅ Field-to-LLVM-index mapping by name
-- ✅ Type unification based on field name matching  
-- ✅ Pattern matching using field names
-- ❌ **NEVER** field ordering dependencies
-- ❌ **NEVER** positional field access in codegen
-- ❌ **NEVER** field index assumptions
+**Compiler Implementation Requirements:**
+- Field-to-LLVM-index mapping must use field name lookup
+- Type unification must be based on field name matching
+- Pattern matching must use field names
+- Positional field access is forbidden in codegen
 
 **❌ FORBIDDEN - Field Access on `any` Types:**
 ```osprey
@@ -508,16 +457,15 @@ let newCounter = counter { value: 5 }
 
 #### Collection Types (List and Map)
 
-**🔥 CRITICAL SPECIFICATION**: Osprey implements **immutable**, **persistent collections** with **zero-cost abstractions** and **compile-time safety**. Collections are **COMPLETELY IMMUTABLE** - operations return new collections without modifying originals.
+Osprey provides immutable, persistent collections with compile-time safety and zero-cost abstractions.
 
 ##### List<T> - Immutable Sequential Collections
 
-**Core Properties:**
-- **Complete Immutability**: Lists cannot be modified after creation
-- **Structural Sharing**: Efficient memory usage through persistent data structures  
-- **Type Safety**: Elements must be homogeneous (same type T)
-- **Bounds Checking**: Array access returns `Result<T, IndexError>` for safety
-- **Zero-Cost Abstraction**: Compiled to efficient native code via C runtime
+**Properties:**
+- Complete immutability with structural sharing
+- Type-safe with homogeneous elements
+- Bounds-checked access returns `Result<T, IndexError>`
+- Compiled to efficient native code
 
 **List Literal Syntax:**
 ```osprey
@@ -727,63 +675,14 @@ let byGrade = groupBy(student => student.grade, students)
 // Map<string, List<Student>> = { "A": [Alice, Charlie], "B": [Bob] }
 ```
 
-**Performance Characteristics:**
-
-**🔥 HIGH-PERFORMANCE C Runtime Integration:**
-
-**List Operations:**
-- **Element Access**: O(1) - direct memory access via C runtime
-- **Concatenation**: O(n) - optimized memory copying in C
-- **Functional Ops**: O(n) - zero-overhead iteration in C
-- **Pattern Matching**: O(1) - compiled to efficient native comparisons
+**Performance:**
 
-**Map Operations:**
-- **Lookup**: O(log n) - persistent hash trie in C runtime
-- **Insert/Update**: O(log n) - structural sharing, minimal allocations
-- **Iteration**: O(n) - cache-friendly traversal patterns
-- **Pattern Matching**: O(log n) - optimized key presence checks
+List operations: O(1) element access, O(n) concatenation and functional operations.
+Map operations: O(log n) lookup/insert/update, O(n) iteration.
 
-**Memory Management:**
-- **Garbage Collection**: Not required - deterministic cleanup via C runtime
-- **Structural Sharing**: Immutable collections share common structure
-- **Copy-on-Write**: Minimal memory overhead for updates
-- **Stack Allocation**: Small collections optimized for stack storage
+Memory management uses structural sharing for efficiency, deterministic cleanup without garbage collection, and stack allocation for small collections.
 
-**Compile-Time Optimizations:**
-```osprey
-// These are optimized at compile time:
-let result = map(x => x * 2, filter(x => x > 5, numbers))
-// Fused into single-pass operation - no intermediate allocations
-
-let lookup = myMap["key"]  
-// Bounds checking eliminated when key presence proven at compile time
-
-let [head, ...tail] = [1, 2, 3]
-// Pattern matching compiled to zero-cost field access
-```
-
-**Safety Guarantees:**
-- **No Buffer Overflows**: All access bounds-checked at compile time or runtime
-- **No Memory Leaks**: Automatic cleanup via C runtime integration
-- **No Race Conditions**: Immutability prevents concurrent modification issues
-- **Type Safety**: All collection operations preserve element types
-
-**Integration with Effects System:**
-```osprey
-// Collections work seamlessly with algebraic effects
-effect Logger {
-    fn log(message: string): unit
-}
-
-fn processItems(items: List<string>) -> unit !Logger = {
-    forEach(item => perform log("Processing: ${item}"), items)
-    perform log("Processed ${toString(length(items))} items")
-}
-
-// Map operations with effects
-fn validateUsers(users: Map<string, User>) -> Map<string, User> !Validator = 
-    mapValues(user => perform validate(user), users)
-```
+Safety: bounds checking prevents overflows, immutability prevents race conditions, type safety enforced throughout.
 
 
 ## Built-in Error Types
@@ -938,80 +837,44 @@ fn complex<T>(x: T, pred: (T) -> bool) -> Option<T> =
 - **Compile-time safety**: All type errors caught before execution
 - **Principal types**: Every expression has a unique most general type
 
-#### 🔥 CRITICAL: Record Type Structural Equivalence
+#### Record Type Structural Equivalence
 
-**MANDATORY REQUIREMENT**: Osprey's Hindley-Milner implementation MUST treat record types using **structural equivalence based EXCLUSIVELY on field names**.
+Osprey's Hindley-Milner implementation uses structural equivalence based on field names only, not field order.
 
-**✅ CORRECT Structural Unification:**
 ```osprey
-// These record types are structurally equivalent (same field names and types)
+// These record types are structurally equivalent
 type PersonA = { name: string, age: int }
-type PersonB = { age: int, name: string }  // Different field ORDER - still equivalent
-
-// Hindley-Milner MUST unify these as the same structural type
-fn processA(p: PersonA) = p.name
-fn processB(p: PersonB) = p.name
+type PersonB = { age: int, name: string }  // Different order, same structure
 
-// These functions MUST be considered type-compatible
-let result1 = processA(PersonB { age: 25, name: "Alice" })  // ✅ MUST work
-let result2 = processB(PersonA { name: "Bob", age: 30 })    // ✅ MUST work
+fn getName(record) = record.name  // Infers: ∀α. {name: string, ...α} -> string
 ```
 
-**✅ POLYMORPHIC Field Access Inference:**
-```osprey
-// Generic field accessor - inferred type based on field NAME only
-fn getName(record) = record.name           // Infers: ∀α. {name: string, ...α} -> string
-fn getAge(record) = record.age            // Infers: ∀α. {age: int, ...α} -> int
-
-// Works with ANY record type that has the named field
-let name1 = getName(Person { name: "Alice", age: 25 })      // ✅ Valid
-let name2 = getName(User { name: "Bob", id: 1, email: "bob@example.com" })  // ✅ Valid
-let age1 = getAge(Person { name: "Alice", age: 25 })       // ✅ Valid
-```
-
-**❌ FORBIDDEN Implementation Approaches:**
-```
-// NEVER ALLOWED in compiler implementation:
-struct_field_0 = llvm_get_field_by_index(record, 0)  // ❌ Positional access
-field_type = type_signature.params[field_position]   // ❌ Position-based type lookup
-unify_by_field_order(record1, record2)              // ❌ Order-dependent unification
-```
+**Unification Algorithm:**
+Record types unify if and only if they have the same field names with matching types. Field order is irrelevant:
 
-**🔥 UNIFICATION ALGORITHM REQUIREMENT:**
 ```
-unify(RecordType1, RecordType2) := 
+unify(RecordType1, RecordType2) :=
     if field_names(RecordType1) ≠ field_names(RecordType2) then FAIL
     else ∀ field_name ∈ field_names(RecordType1):
         unify(field_type(RecordType1, field_name), field_type(RecordType2, field_name))
-        
-// Field ordering is IRRELEVANT - only field names and their types matter
 ```
 
 #### Polymorphic Type Variables vs Any Type
 
-**CRITICAL DISTINCTION**: Hindley-Milner infers polymorphic type variables (α, β, γ), NOT the `any` type.
+Hindley-Milner infers polymorphic type variables (α, β, γ), not the `any` type:
 
-**✅ HINDLEY-MILNER POLYMORPHISM:**
 ```osprey
-fn identity(x) = x                    // Infers: <T>(T) -> T (polymorphic)
-fn getFirst(p) = p.first             // Infers: <A, B>(Pair<A, B>) -> A
-fn apply(f, x) = f(x)                // Infers: <A, B>((A) -> B, A) -> B
+fn identity(x) = x           // Infers: <T>(T) -> T
+fn apply(f, x) = f(x)        // Infers: <A, B>((A) -> B, A) -> B
 ```
 
-**❌ ANY TYPE (Requires Explicit Declaration):**
-```osprey
-fn parseValue(input: string) -> any = processInput(input)  // Explicit any
-fn getDynamicValue() -> any = readFromConfig()             // Explicit any
-```
+The `any` type requires explicit declaration:
 
-**Type Variable Instantiation**: Polymorphic type variables are instantiated to concrete types at usage sites:
 ```osprey
-let intId = identity(42)        // T := int
-let stringId = identity("test") // T := string
-let boolId = identity(true)     // T := bool
+fn parseValue(input: string) -> any = processInput(input)
 ```
 
-**Safety Guarantee**: Polymorphic types are statically safe - all type checking occurs at compile time with no runtime type uncertainty.
+Polymorphic type variables are instantiated at call sites and checked statically at compile time.
 
 #### Hindley-Milner Constraint Resolution
 
diff --git a/compiler/spec/0005-FunctionCalls.md b/compiler/spec/0005-FunctionCalls.md
index 289eda6..146fcfe 100644
--- a/compiler/spec/0005-FunctionCalls.md
+++ b/compiler/spec/0005-FunctionCalls.md
@@ -1,48 +1,61 @@
-6. [Function Calls](0006-FunctionCalls.md)
-   - [Named Arguments Requirement](#named-arguments-requirement)
-       - [Valid Function Calls](#valid-function-calls)
-       - [Invalid Function Calls](#invalid-function-calls)
-   - [Function Call Compilation Rules](#function-call-compilation-rules)
+# Function Calls
 
-## Function Calls
+## Named Arguments Requirement
 
-### Named Arguments Requirement
+Functions with more than one parameter must be called with named arguments.
 
-**CRITICAL RULE**: Functions with more than one parameter **MUST** be called with named arguments.
-
-#### Valid Function Calls
+### Valid Function Calls
 
 ```osprey
+// Zero parameters
+fn getValue() = 42
+let value = getValue()
+
 // Single parameter - positional allowed
 fn double(x) = x * 2
 let result = double(5)
 
-// Zero parameters - no arguments
-fn getValue() = 42
-let value = getValue()
-
 // Multiple parameters - named arguments required
 fn add(x, y) = x + y
 let sum = add(x: 10, y: 20)
 
-// Multiple parameters - order doesn't matter with named args
+// Order doesn't matter with named arguments
 let sum2 = add(y: 20, x: 10)
+
+// Works with type annotations
+fn multiply(a: int, b: int) -> int = a * b
+let product = multiply(a: 5, b: 3)
 ```
 
-#### Invalid Function Calls
+### Invalid Function Calls
 
 ```osprey
 // ERROR: Multi-parameter function with positional arguments
 fn add(x, y) = x + y
-let sum = add(10, 20)  // ❌ Compilation error
+let sum = add(10, 20)  // Compilation error
 
 // ERROR: Mixed positional and named arguments
-let sum = add(10, y: 20)  // ❌ Compilation error
+let sum = add(10, y: 20)  // Compilation error
+
+// ERROR: Missing parameter name
+let result = multiply(5, b: 3)  // Compilation error
 ```
 
-### Function Call Compilation Rules
+## Compilation Rules
+
+1. **Zero parameters**: Called with empty parentheses `()`
+2. **Single parameter**: May use positional or named argument
+3. **Multiple parameters**: All arguments must be named
+4. **Argument order**: Named arguments are reordered to match parameter declaration order during compilation
+
+## Rationale
+
+Named arguments improve readability and prevent argument order errors in multi-parameter functions:
+
+```osprey
+// Clear intent with named arguments
+httpGet(clientID: client, path: "/users", headers: "")
 
-1. **Single Parameter Functions**: May use positional arguments
-2. **Zero Parameter Functions**: Called with empty parentheses `()`
-3. **Multi-Parameter Functions**: Must use named arguments for ALL parameters
-4. **Argument Reordering**: Named arguments are reordered to match parameter declaration order
\ No newline at end of file
+// Unclear with positional arguments (forbidden)
+httpGet(client, "/users", "")  // What does "" mean?
+```
\ No newline at end of file
diff --git a/compiler/spec/0006-StringInterpolation.md b/compiler/spec/0006-StringInterpolation.md
index 3dd8251..2abd1c2 100644
--- a/compiler/spec/0006-StringInterpolation.md
+++ b/compiler/spec/0006-StringInterpolation.md
@@ -1,16 +1,10 @@
-7. [String Interpolation](0007-StringInterpolation.md)
-   - [Syntax](#syntax)
-   - [Expression Support](#expression-support)
-   - [Type Handling](#type-handling)
-   - [Implementation](#implementation)
-
 # String Interpolation
 
-✅ **IMPLEMENTED**: String interpolation is fully implemented and working with comprehensive test coverage.
+String interpolation provides convenient inline expression evaluation within string literals.
 
 ## Syntax
 
-String interpolation uses `${}` syntax within double-quoted strings:
+String interpolation uses `${}` syntax:
 
 ```osprey
 let name = "Alice"
@@ -20,7 +14,7 @@ let message = "Hello ${name}, you are ${age} years old"
 
 ## Expression Support
 
-Any expression is valid inside interpolation:
+Any expression can be interpolated:
 
 ```osprey
 let x = 10
@@ -28,17 +22,61 @@ let y = 5
 print("Sum: ${x + y}")
 print("Product: ${x * y}")
 print("Complex: ${(x + y) * 2 - 1}")
+
+// Function calls
+fn double(n) = n * 2
+print("Doubled: ${double(5)}")
+
+// Field access
+type Person = { name: string, age: int }
+let person = Person { name: "Bob", age: 25 }
+print("Person: ${person.name}, age ${person.age}")
 ```
 
 ## Type Handling
 
-- **String variables**: Use `%s` format specifier
-- **Integer expressions**: Use `%ld` format specifier  
-- **Function calls**: Supported for single-parameter functions
+Interpolated expressions are automatically converted to strings:
+
+- **Primitive types**: int, float, bool converted directly
+- **String types**: Inserted as-is
+- **Result types**: Must be pattern-matched before interpolation
+- **Complex types**: Use `toString()` for explicit conversion
+
+```osprey
+let num = 42
+let flag = true
+print("Number: ${num}, Flag: ${flag}")
+
+// Result types require unwrapping
+let result = 10 + 5
+match result {
+    Success { value } => print("Result: ${value}")
+    Error { message } => print("Error: ${message}")
+}
+```
+
+## Escaping
+
+Use backslash to escape special characters:
+
+```osprey
+let literal = "Dollar sign: \${not interpolated}"
+let newline = "Line 1\nLine 2"
+let quote = "He said \"Hello\""
+let backslash = "Path: C:\\Users\\Name"
+```
+
+Supported escape sequences:
+- `\n` - Newline
+- `\t` - Tab
+- `\r` - Carriage return
+- `\\` - Backslash
+- `\"` - Double quote
+- `\${` - Literal `${` (prevents interpolation)
 
 ## Implementation
 
-Interpolated strings are compiled to:
+Interpolated strings compile to efficient buffer operations:
 1. Allocate a buffer (`alloca [1024 x i8]`)
-2. Use `sprintf` to format the string
-3. Use `puts` to output the result
\ No newline at end of file
+2. Use `sprintf` with appropriate format specifiers (`%s`, `%ld`, etc.)
+3. Return the formatted string for use in expressions
\ No newline at end of file
diff --git a/compiler/spec/0007-PatternMatching.md b/compiler/spec/0007-PatternMatching.md
index f026b65..cc122a0 100644
--- a/compiler/spec/0007-PatternMatching.md
+++ b/compiler/spec/0007-PatternMatching.md
@@ -11,9 +11,7 @@
 
 ## Pattern Matching
 
-**🔥 CRITICAL SPECIFICATION**: Pattern matching in Osprey MUST use **FIELD NAME MATCHING ONLY**. Pattern matching on record types is based on **structural equivalence by field names**, never field ordering or positioning.
-
-**IMPLEMENTATION REQUIREMENT**: The compiler MUST implement pattern matching using field name lookup and structural type unification as specified in the Hindley-Milner Type Inference requirements (see [Type System](0004-TypeSystem.md#hindley-milner-type-inference)).
+Pattern matching in Osprey uses field name matching only. Record type patterns are based on structural equivalence by field names, not field order. See [Type System](0004-TypeSystem.md#hindley-milner-type-inference) for complete type unification rules.
 
 ### Basic Patterns
 
@@ -141,7 +139,7 @@ match anyValue {
 
 ## Result Type Pattern Matching (Arithmetic Expressions)
 
-**🔥 CRITICAL**: All arithmetic expressions return `Result<T, MathError>`. You **MUST** handle them with pattern matching.
+All arithmetic expressions return `Result<T, MathError>` and must be handled with pattern matching. The compiler automatically unwraps intermediate Results in nested arithmetic, so only the final result requires pattern matching.
 
 **✨ KEY INSIGHT**: Nested arithmetic expressions do NOT require nested pattern matching! The compiler automatically unwraps intermediate Results, so you only pattern match the final result.
 
@@ -155,61 +153,28 @@ match calculation {
 }
 ```
 
-### Compound Expression Examples (CRYSTAL CLEAR)
-```osprey
-// Each of these returns a SINGLE Result for the ENTIRE expression
-// NO nested Results - auto-unwrapping handles intermediate operations!
-let simple = 10 + 5                    // Result<int, MathError> - NOT Result<Result<...>>
-let complex = 1 + 2 * 3 - 4 / 2        // Result<int, MathError> - NOT Result<Result<...>>
-let nested = ((a + b) * c) / (d - e)   // Result<int, MathError> - NOT Result<Result<...>>
+### Compound Arithmetic Expressions
 
-// Handle ALL of them the SAME WAY - single pattern match!
-match simple {
-    Success { value } => print("10 + 5 = ${value}")
-    Error { message } => print("Failed: ${message}")
-}
+Nested arithmetic expressions return a single Result, not nested Results:
 
-match complex {
-    Success { value } => print("Complex calc = ${value}")
-    Error { message } => print("Overflow/error: ${message}")
-}
+```osprey
+let simple = 10 + 5                    // Result<int, MathError>
+let complex = 1 + 2 * 3 - 4 / 2        // Result<int, MathError>
+let nested = ((a + b) * c) / (d - e)   // Result<int, MathError>
 
-match nested {
-    Success { value } => print("Nested result = ${value}")
-    Error { message } => print("Division by zero or overflow: ${message}")
+// All handled the same way
+match simple {
+    Success { value } => print("Result: ${value}")
+    Error { message } => print("Error: ${message}")
 }
 ```
 
-### Auto-Unwrapping Explained
+The compiler auto-unwraps intermediate Results in arithmetic chains:
+
 ```osprey
-// Example: (10 + 5) * 2
-// Step 1: 10 + 5 produces Result<int, MathError>
-// Step 2: Compiler auto-unwraps the Result to get the int value
-// Step 3: Multiply the unwrapped value by 2
-// Step 4: Wrap in a new Result<int, MathError>
-// Final: ONE Result, not nested!
-
-let example = (10 + 5) * 2  // Result<int, MathError>
+let example = (10 + 5) * 2  // Single Result<int, MathError>
 match example {
-    Success { value } => print(value)  // Prints: 30
-    Error { message } => print(message)
-}
-
-// NO nested matching required!
-// ❌ WRONG - you do NOT need this:
-// match (10 + 5) {
-//     Success { innerValue } => {
-//         match innerValue * 2 {
-//             Success { value } => print(value)
-//             ...
-//         }
-//     }
-// }
-
-// ✅ CORRECT - just match the final result:
-let result = (10 + 5) * 2
-match result {
-    Success { value } => print(value)
+    Success { value } => print(value)  // 30
     Error { message } => print(message)
 }
 ```
diff --git a/compiler/spec/0010-LoopConstructsAndFunctionalIterators.md b/compiler/spec/0010-LoopConstructsAndFunctionalIterators.md
index 50724d9..8f4ab96 100644
--- a/compiler/spec/0010-LoopConstructsAndFunctionalIterators.md
+++ b/compiler/spec/0010-LoopConstructsAndFunctionalIterators.md
@@ -20,16 +20,11 @@
 
 # Loop Constructs and Functional Iterators
 
-✅ **FULLY IMPLEMENTED**: All core iterator functions (`range`, `forEach`, `map`, `filter`, `fold`) are fully implemented with stream fusion optimization. The pipe operator (`|>`) enables elegant function composition. Map and filter use zero-cost abstractions via compile-time stream fusion.
+Osprey is a functional language without imperative loop constructs. Iteration uses functional patterns with the core functions `range`, `forEach`, `map`, `filter`, and `fold`, composed with the pipe operator `|>`.
 
-## Functional Iteration Philosophy
+## Functional Iteration
 
-**Osprey is a functional language and does NOT support imperative loop constructs.** Instead, Osprey provides powerful functional iteration patterns that are:
-
-1. **Composable** - Functional iterators can be chained with `|>`
-2. **Safe** - No mutable state, no infinite loop bugs
-3. **Concurrent** - Fibers provide better parallelism than loops
-4. **Testable** - Pure functions are easier to test than stateful loops
+Functional iteration provides composable, safe patterns without mutable state. Fibers handle concurrent iteration, and pure functions simplify testing.
 
 ## Core Iterator Functions
 
@@ -188,25 +183,15 @@ input()
   |> print
 ```
 
-## Why No Imperative Loops?
+## Alternative to Imperative Loops
 
-**Anti-Pattern:**
-```osprey
-// ❌ WRONG - Imperative loops (NOT SUPPORTED)
-loop {
-    let request = getRequest()
-    processRequest(request)
-}
-```
+Use functional patterns instead of imperative loops:
 
-**Functional Pattern:**
 ```osprey
-// ✅ CORRECT - Functional approach
-fn serverHandler() -> Unit = {
-    requestStream() 
+// Functional approach
+fn serverHandler() -> unit = {
+    requestStream()
     |> map(processRequest)
     |> forEach(sendResponse)
 }
-```
-
-This functional approach provides better maintainability, testability, and performance than traditional imperative loops. 
\ No newline at end of file
+``` 
\ No newline at end of file
diff --git a/compiler/spec/0013-ErrorHandling.md b/compiler/spec/0013-ErrorHandling.md
index ff16ec3..15be378 100644
--- a/compiler/spec/0013-ErrorHandling.md
+++ b/compiler/spec/0013-ErrorHandling.md
@@ -30,30 +30,22 @@ match result {
 
 This approach guarantees that error handling is explicit, robust, and checked at compile time.
 
-### Arithmetic Safety and Result Types
+### Arithmetic Operations and Result Types
 
-**🚨 CRITICAL DESIGN PRINCIPLE 🚨**: ALL arithmetic operations (`+`, `-`, `*`, `/`, `%`) return `Result<T, MathError>` because they can **ALL** fail (overflow, underflow, division by zero).
+All arithmetic operations return `Result<T, MathError>` to handle overflow, underflow, and division by zero:
 
-## **THE GOLDEN RULE:**
+**Operator Signatures:**
+- `+` Addition: `(int, int) -> Result<int, MathError>`
+- `-` Subtraction: `(int, int) -> Result<int, MathError>`
+- `*` Multiplication: `(int, int) -> Result<int, MathError>`
+- `/` Division: `(int, int) -> Result<float, MathError>` — always returns float
+- `%` Modulo: `(int, int) -> Result<int, MathError>`
 
-**ALL Arithmetic Operations Return Result Types:**
-- `+` Addition: `(int, int) -> Result<int, MathError>` - Can overflow
-- `-` Subtraction: `(int, int) -> Result<int, MathError>` - Can underflow
-- `*` Multiplication: `(int, int) -> Result<int, MathError>` - Can overflow
-- `/` Division: `(int, int) -> Result<float, MathError>` - Can divide by zero, ALWAYS returns float
-- `%` Modulo: `(int, int) -> Result<int, MathError>` - Can divide by zero
-
-**Why ALL operations return Result:**
-- **Addition/Subtraction**: Can overflow/underflow (e.g., MAX_INT + 1)
-- **Multiplication**: Can overflow (e.g., 1000000 * 1000000)
-- **Division**: Can divide by zero, ALWAYS returns float for mathematical correctness
-- **Modulo**: Can divide by zero
-
-**Type Promotion Rules:**
+**Type Promotion:**
 - `int ⊕ int` → `Result<int, MathError>` (where ⊕ is +, -, *, %)
 - `float ⊕ float` → `Result<float, MathError>`
 - `int ⊕ float` → `Result<float, MathError>` (int promoted to float)
-- `int / int` → `Result<float, MathError>` (division ALWAYS returns float!)
+- `int / int` → `Result<float, MathError>` (division always returns float)
 
 #### Arithmetic Examples
 
@@ -104,25 +96,17 @@ print(10 / 0)                      // Outputs: Error(DivisionByZero)
 
 ### Result Type toString Format
 
-When converting a `Result` type to a string using `toString()`, the format **MUST ALWAYS** be:
-- **`Success(value)`**: For successful results
-- **`Error(message)`**: For error results
+Result types convert to strings in the format `Success(value)` or `Error(message)`:
 
-**Examples:**
 ```osprey
 let divisionResult = 15 / 3              // Result<float, MathError>
-print(toString(divisionResult))          // Outputs: "Success(5)"
+print(toString(divisionResult))          // "Success(5)"
 
 let divisionByZero = 10 / 0              // Result<float, MathError>
-print(toString(divisionByZero))          // Outputs: "Error(DivisionByZero)"
+print(toString(divisionByZero))          // "Error(DivisionByZero)"
 
 let calculation = 10 + 5                 // Result<int, MathError>
-print(toString(calculation))             // Outputs: "Success(15)"
+print(toString(calculation))             // "Success(15)"
 ```
 
-**ABSOLUTE RULES:**
-- ✅ **ALWAYS** wrap values in `Success(...)` or `Error(...)`
-- ❌ **NEVER** output raw values without the wrapper
-- ❌ **NEVER** use different formats for different Result types
-
-This ensures consistent, predictable string representations of Result types across the entire language.
\ No newline at end of file
+This format is consistent across all Result types.
\ No newline at end of file
diff --git a/compiler/spec/0017-AlgebraicEffects.md b/compiler/spec/0017-AlgebraicEffects.md
index 612fe0d..a73ec1f 100644
--- a/compiler/spec/0017-AlgebraicEffects.md
+++ b/compiler/spec/0017-AlgebraicEffects.md
@@ -147,16 +147,16 @@ fn loggedCalculation<E>(x: Int) -> Int !E = {
 3. **Operation Resolution**: Each `perform` resolves to its handler
 4. **Code Generation**: Generate efficient handler dispatch
 
-**Revolutionary Safety**: Unlike other effect systems, unhandled effects cause **compile-time errors**, never runtime crashes.
+Unhandled effects cause compile-time errors, ensuring safety.
 
 ### Comparison with Research
 
-| Aspect                | Plotkin & Pretnar Theory | Osprey Implementation         |
-| --------------------- | ------------------------ | ----------------------------- |
-| **Effect Operations** | Free algebraic theory    | `effect` declarations         |
-| **Handlers**          | Models of the theory     | `handle...in` expressions     |
-| **Handling**          | Unique homomorphisms     | Compile-time dispatch         |
-| **Safety**            | Theoretical correctness  | **Compile-time verification** |
+| Aspect                | Plotkin & Pretnar Theory | Osprey Implementation     |
+| --------------------- | ------------------------ | ------------------------- |
+| **Effect Operations** | Free algebraic theory    | `effect` declarations     |
+| **Handlers**          | Models of the theory     | `handle...in` expressions |
+| **Handling**          | Unique homomorphisms     | Compile-time dispatch     |
+| **Safety**            | Theoretical correctness  | Compile-time verification |
 
 ### Examples
 
@@ -201,51 +201,34 @@ in
 
 ---
 
-## **OSPREY'S REVOLUTIONARY EFFECT SAFETY - BEYOND THE RESEARCH**
+## Compile-Time Effect Verification
 
-### **COMPILE-TIME EFFECT VERIFICATION**
-
-While Plotkin & Pretnar established the theoretical foundation, Osprey implements **the first practical effect system with complete compile-time safety**:
-
-**🚨 UNHANDLED EFFECTS = COMPILATION ERROR (NOT RUNTIME ERROR!) 🚨**
+Osprey provides complete compile-time safety for algebraic effects. Unhandled effects produce compilation errors, not runtime failures:
 
 ```osprey
-effect Logger { log: fn(String) -> Unit }
+effect Logger { log: fn(string) -> unit }
 
-fn main() -> Unit = {
-    perform Logger.log("This will fail compilation!")  // ❌ COMPILATION ERROR
+fn main() -> unit = {
+    perform Logger.log("This will fail compilation!")  // Compilation error
 }
 ```
 
-**Error**: `COMPILATION ERROR: Unhandled effect 'Logger.log' - all effects must be explicitly handled or forwarded in function signatures.`
-
-### **SUPERIORITY TO OTHER IMPLEMENTATIONS**
-
-| System            | Theoretical Basis       | Runtime Safety | Compile-time Safety         |
-| ----------------- | ----------------------- | -------------- | --------------------------- |
-| **OCaml Effects** | Plotkin & Pretnar       | ❌ Crashes      | ❌ No verification           |
-| **Eff Language**  | Plotkin & Pretnar       | ❌ Exceptions   | ❌ Partial checking          |
-| **Koka Effects**  | Plotkin & Pretnar       | ❌ Aborts       | ⚠️ Effect inference          |
-| **🔥 OSPREY 🔥**    | **Plotkin & Pretnar +** | ✅ **Safe**     | ✅ **Complete verification** |
-
-### **IMPLEMENTATION INNOVATION**
+**Error**: Unhandled effect 'Logger.log' - all effects must be explicitly handled or forwarded in function signatures.
 
-Osprey extends the theoretical foundation with:
+### Comparison with Other Effect Systems
 
-1. **Complete static verification** - No unhandled effects reach runtime
-2. **Effect inference** - Minimal effect annotations required  
-3. **Efficient compilation** - Zero-cost when no handlers present
-4. **Composable handlers** - Clean nesting and effect forwarding
+| System        | Theoretical Basis | Runtime Safety | Compile-time Safety       |
+| ------------- | ----------------- | -------------- | ------------------------- |
+| OCaml Effects | Plotkin & Pretnar | Crashes        | No verification           |
+| Eff Language  | Plotkin & Pretnar | Exceptions     | Partial checking          |
+| Koka Effects  | Plotkin & Pretnar | Aborts         | Effect inference          |
+| Osprey        | Plotkin & Pretnar | Safe           | Complete verification     |
 
-**🚀 OSPREY: ALGEBRAIC EFFECTS THEORY REALIZED WITH TOTAL SAFETY! 🚀**
+Osprey extends the theoretical foundation with complete static verification, effect inference, efficient compilation, and composable handlers.
 
-## **CIRCULAR DEPENDENCY DETECTION - REVOLUTIONARY SAFETY**
+## Circular Dependency Detection
 
-### **COMPILE-TIME CIRCULAR DEPENDENCY DETECTION**
-
-Osprey implements **the world's first effect system with complete circular dependency detection** at compile time:
-
-**🚨 CIRCULAR EFFECT DEPENDENCIES = COMPILATION ERROR (NOT RUNTIME STACK OVERFLOW!) 🚨**
+Osprey detects circular effect dependencies at compile time:
 
 ```osprey
 effect StateA { getFromB: fn() -> int }
@@ -264,11 +247,9 @@ fn main() -> Unit =
           circularA  // Would cause infinite recursion
 ```
 
-**Error**: `COMPILATION ERROR: Circular effect dependency detected - handler StateA.getFromB calls function that performs StateB.getFromA, which is handled by calling StateA.getFromB (infinite recursion detected)`
+**Error**: Circular effect dependency detected - handler StateA.getFromB calls function that performs StateB.getFromA, which is handled by calling StateA.getFromB (infinite recursion detected)
 
-### **INFINITE HANDLER RECURSION DETECTION**
-
-**🚨 HANDLERS CALLING THEMSELVES = COMPILATION ERROR! 🚨**
+### Infinite Handler Recursion Detection
 
 ```osprey
 effect Counter { increment: fn(int) -> int }
@@ -282,29 +263,27 @@ fn main() -> Unit =
         performIncrement 5  // Would cause stack overflow
 ```
 
-**Error**: `COMPILATION ERROR: Infinite handler recursion detected - handler Counter.increment calls function that performs the same effect it handles (infinite recursion detected)`
-
-### **SAFETY GUARANTEES**
+**Error**: Infinite handler recursion detected - handler Counter.increment calls function that performs the same effect it handles (infinite recursion detected)
 
-| **Safety Check**          | **Osprey**      | **Other Languages** |
-| ------------------------- | --------------- | ------------------- |
-| **Unhandled Effects**     | ✅ Compile Error | ❌ Runtime Crash     |
-| **Circular Dependencies** | ✅ Compile Error | ❌ Stack Overflow    |
-| **Handler Recursion**     | ✅ Compile Error | ❌ Infinite Loop     |
-| **Effect Type Safety**    | ✅ Complete      | ⚠️ Partial           |
+### Safety Guarantees
 
-### **STATIC ANALYSIS ALGORITHM**
+| Safety Check          | Osprey         | Other Languages |
+| --------------------- | -------------- | --------------- |
+| Unhandled Effects     | Compile Error  | Runtime Crash   |
+| Circular Dependencies | Compile Error  | Stack Overflow  |
+| Handler Recursion     | Compile Error  | Infinite Loop   |
+| Effect Type Safety    | Complete       | Partial         |
 
-Osprey's compiler performs **static call graph analysis** to detect:
+### Static Analysis
 
-1. **Effect Dependency Graphs** - Maps which effects depend on which others
-2. **Handler Call Chains** - Traces handler execution paths
-3. **Cycle Detection** - Uses topological sorting to find circular dependencies
-4. **Recursion Analysis** - Detects when handlers call functions that perform the same effect
+The compiler performs static call graph analysis:
 
-**Revolutionary Result**: **NO EFFECT-RELATED RUNTIME ERRORS ARE POSSIBLE**
+1. Effect dependency graphs map which effects depend on others
+2. Handler call chains trace execution paths
+3. Cycle detection uses topological sorting
+4. Recursion analysis detects handlers calling functions that perform the same effect
 
-**🔥 OSPREY: THE ONLY LANGUAGE WITH MATHEMATICALLY PROVEN EFFECT SAFETY! 🔥**
+This ensures no effect-related runtime errors are possible.
 
 [1]: https://www.ospreylang.dev/spec/ "Osprey Language Specification - Osprey Programming Language"
 
@@ -321,138 +300,115 @@ https://en.wikipedia.org/wiki/Effect_system
 https://dl.acm.org/doi/pdf/10.1145/3290319
 
 
-## Completeness Report
+## Implementation Status
 
-## 📋 ALGEBRAIC EFFECTS VERIFICATION REPORT
+Analysis of Osprey's implementation against Plotkin & Pretnar's algebraic effects theory:
 
-Based on:
-https://arxiv.org/pdf/1312.1399
-
-After thorough analysis of Osprey's implementation against Plotkin & Pretnar's paper, here's my comprehensive verification:
+## Correctly Implemented
 
-## ✅ CORRECTLY IMPLEMENTED ASPECTS
-
-### 1. **Effect Declarations** ✅
+### Effect Declarations
 - **Paper**: `op : α → β` (operation signatures)
 - **Osprey**: `effect EffectName { operationName: fn(α) -> β }`
-- **Verdict**: ✅ CORRECT - Perfect mapping to the paper's operation signatures
+- **Status**: Correct mapping to paper's operation signatures
 
-### 2. **Perform Expressions** ✅
+### Perform Expressions
 - **Paper**: `opV(x : β. M)` (operation with continuation)
 - **Osprey**: `perform EffectName.operationName(args)`
-- **Verdict**: ✅ CORRECT - Implicit continuation handling matches theory
+- **Status**: Correct - implicit continuation handling matches theory
 
-### 3. **Handler Syntax** ✅
+### Handler Syntax
 - **Paper**: `{opx : α(k : β → C) → Mop}`
 - **Osprey**: `handle EffectName operationName params => body in expr`
-- **Verdict**: ✅ CORRECT - Clean syntax mapping to theoretical foundation
+- **Status**: Correct syntax mapping to theoretical foundation
 
-### 4. **Compile-Time Safety** ✅ **REVOLUTIONARY**
+### Compile-Time Safety
 - **Paper**: Theoretical foundation only
-- **Osprey**: **WORLD-FIRST** compile-time unhandled effect detection
-- **Verdict**: ✅ EXCEEDS PAPER - Osprey goes beyond theory with revolutionary safety
+- **Osprey**: Compile-time unhandled effect detection
+- **Status**: Exceeds paper - goes beyond theory with compile-time verification
 
-### 5. **Effect Type System** ✅
+### Effect Type System
 - **Paper**: Effect annotations and inference
 - **Osprey**: `fn name() -> Type !Effect` syntax
-- **Verdict**: ✅ CORRECT - Proper effect type annotations
+- **Status**: Correct effect type annotations
 
-### 6. **Nested Handlers** ✅
+### Nested Handlers
 - **Paper**: Handler composition and nesting
 - **Osprey**: Multiple nested `handle...in` expressions
-- **Verdict**: ✅ CORRECT - Proper lexical scoping
+- **Status**: Correct lexical scoping
 
-## ❌ CRITICAL MISSING FEATURES
+## Missing Features
 
-### 1. **Continuation/Resume Operations** ❌ **CRITICAL GAP**
+### Continuation/Resume Operations
 - **Paper**: Handlers have `k : β → C` continuations, explicit `resume(value)`
 - **Osprey**: **MISSING** - No `resume` operations implemented
 - **Impact**: **MAJOR** - This is fundamental to algebraic effects theory
 - **Status**: Documented as "COMING SOON" in README
 
-### 2. **Proper Handler Semantics** ❌ **THEORETICAL VIOLATION**
+### Handler Semantics
 - **Paper**: Handlers must handle the continuation explicitly
-- **Osprey**: Current handlers are just simple value substitutions
-- **Impact**: **CRITICAL** - Not true algebraic effects without continuations
-- **Example Missing**:
-  ```osprey
-  handle State
-    get k => k(42)        // Should resume with value
-    set value k => k(())  // Should resume with unit
-  ```
+- **Osprey**: Current handlers use simple value substitutions
+- **Status**: Not fully implementing true algebraic effects without continuations
 
-### 3. **CPS Transformation** ❌ **IMPLEMENTATION GAP**
+### CPS Transformation
 - **Paper**: Requires continuation-passing style transformation
-- **Osprey**: Infrastructure exists but not complete
-- **Impact**: **MAJOR** - Cannot properly suspend/resume computation
-
-## ⚠️ PARTIALLY IMPLEMENTED FEATURES
-
-### 1. **Handler Execution** ⚠️
-- **Status**: Parsing works, but execution is incomplete
-- **Issue**: No proper continuation capture/restoration
-- **Evidence**: Multiple examples in `failscompilation/` directory
-
-### 2. **Multi-Effect Composition** ⚠️
-- **Status**: `![Effect1, Effect2]` syntax exists
-- **Issue**: Complex interaction semantics not fully implemented
-
-## 🔥 OSPREY'S REVOLUTIONARY INNOVATIONS
-
-### 1. **Compile-Time Effect Safety** 🚀
-- **WORLD-FIRST**: 100% compile-time unhandled effect detection
-- **SUPERIORITY**: Other languages crash at runtime, Osprey prevents compilation
-- **EVIDENCE**: Comprehensive test suite in `failscompilation/`
-
-### 2. **Circular Dependency Detection** 🚀
-- **INNOVATION**: Static analysis prevents infinite handler recursion
-- **SAFETY**: Detects circular effect dependencies at compile time
-- **UNIQUE**: No other language has this level of effect safety
-
-### 3. **Fiber Integration** 🚀
-- **INNOVATION**: Effects system integrated with lightweight fibers
-- **BENEFIT**: Type-safe concurrency with effect tracking
-- **EVIDENCE**: Multiple fiber+effects examples working
-
-## 📊 OVERALL ASSESSMENT
-
-| Aspect | Paper Requirement | Osprey Status | Grade |
-|--------|------------------|---------------|--------|
-| **Effect Declarations** | ✅ Required | ✅ Complete | **A+** |
-| **Perform Operations** | ✅ Required | ✅ Complete | **A+** |
-| **Handler Syntax** | ✅ Required | ✅ Complete | **A+** |
-| **Continuations/Resume** | ✅ **CRITICAL** | ❌ **MISSING** | **F** |
-| **Handler Semantics** | ✅ **CRITICAL** | ❌ **INCOMPLETE** | **D** |
-| **CPS Transformation** | ✅ Required | ⚠️ Partial | **C** |
-| **Compile-Time Safety** | ⚠️ Not specified | ✅ **REVOLUTIONARY** | **A++** |
-| **Effect Type System** | ✅ Required | ✅ Complete | **A+** |
-
-## 🎯 FINAL VERDICT
-
-**OSPREY'S ALGEBRAIC EFFECTS: PARTIALLY CORRECT WITH REVOLUTIONARY INNOVATIONS**
-
-### ✅ **STRENGTHS**
-- **Perfect syntax mapping** to Plotkin & Pretnar theory
-- **Revolutionary compile-time safety** (world-first)
-- **Excellent type system** integration
-- **Comprehensive test coverage** for implemented features
-
-### ❌ **CRITICAL GAPS**
-- **Missing continuation/resume operations** (fundamental to algebraic effects)
-- **Incomplete handler semantics** (not true algebraic effects without continuations)
-- **CPS transformation incomplete** (cannot properly suspend/resume)
-
-### 🚀 **REVOLUTIONARY ASPECTS**
-- **100% compile-time effect safety** (exceeds all other implementations)
-- **Circular dependency detection** (unique innovation)
-- **Fiber integration** (novel combination)
-
-## 🔥 **RECOMMENDATION**
-
-**OSPREY NEEDS TO IMPLEMENT CONTINUATIONS/RESUME TO BE THEORETICALLY CORRECT**
-
-While Osprey has revolutionary safety features that exceed the paper's requirements, the **missing continuation mechanism is a fundamental theoretical gap**. The current implementation is more like "effect substitution" than true algebraic effects.
-
-**Priority Fix**: Implement `resume(value)` operations in handlers to enable proper continuation-based semantics as defined in Plotkin & Pretnar's paper.
-
-**Bottom Line**: Osprey is **80% theoretically correct** with **revolutionary practical innovations** that surpass all other implementations in safety guarantees.
+- **Osprey**: Infrastructure exists but incomplete
+- **Status**: Cannot properly suspend/resume computation
+
+## Partially Implemented
+
+### Handler Execution
+- Parsing works, but execution is incomplete
+- No proper continuation capture/restoration
+- Multiple examples in `failscompilation/` directory
+
+### Multi-Effect Composition
+- `![Effect1, Effect2]` syntax exists
+- Complex interaction semantics not fully implemented
+
+## Osprey's Innovations
+
+### Compile-Time Effect Safety
+- 100% compile-time unhandled effect detection
+- Other languages crash at runtime; Osprey prevents compilation
+- Comprehensive test suite in `failscompilation/`
+
+### Circular Dependency Detection
+- Static analysis prevents infinite handler recursion
+- Detects circular effect dependencies at compile time
+
+### Fiber Integration
+- Effects system integrated with lightweight fibers
+- Type-safe concurrency with effect tracking
+
+## Overall Assessment
+
+| Aspect                    | Paper Requirement | Osprey Status | Assessment |
+| ------------------------- | ----------------- | ------------- | ---------- |
+| Effect Declarations       | Required          | Complete      | Correct    |
+| Perform Operations        | Required          | Complete      | Correct    |
+| Handler Syntax            | Required          | Complete      | Correct    |
+| Continuations/Resume      | Critical          | Missing       | Gap        |
+| Handler Semantics         | Critical          | Incomplete    | Gap        |
+| CPS Transformation        | Required          | Partial       | Gap        |
+| Compile-Time Safety       | Not specified     | Complete      | Innovation |
+| Effect Type System        | Required          | Complete      | Correct    |
+
+## Summary
+
+**Strengths:**
+- Correct syntax mapping to Plotkin & Pretnar theory
+- Compile-time safety exceeds theoretical requirements
+- Strong type system integration
+- Comprehensive test coverage for implemented features
+
+**Gaps:**
+- Missing continuation/resume operations (fundamental to algebraic effects)
+- Incomplete handler semantics (not full algebraic effects without continuations)
+- CPS transformation incomplete (cannot properly suspend/resume)
+
+**Innovations:**
+- Complete compile-time effect safety
+- Circular dependency detection
+- Fiber integration with effects
+
+Osprey provides approximately 80% theoretical correctness with practical innovations that surpass other implementations in safety guarantees. Full algebraic effects support requires implementing `resume(value)` operations in handlers for proper continuation-based semantics.