3. Prevent duplicate work🔗

To achieve goal (2), reduce code duplication in the analysis of popular languages, Laurel contains many features shared between several languages. The following table shows which features are shared with which input languages. Laurel is currently prioritizing support for statically and dynmically typed language with garbage collection, but we expect to at some point also add support for things like pointers to support a language like C.

Legend: the Laurel column records Laurel's own status — ✓ implemented, WIP planned but not yet implemented, ✗ not planned. The Core column records what Strata Core, Laurel's lowering target, provides natively — ✓ a native construct, ~ expressible only by encoding (for example via maps or axioms rather than a dedicated construct), — no support (Laurel must lower the feature away rather than pass it through). The source-language columns (Java, JavaScript, Python, C) record — ✓ directly supported, ~ partial or library-only (semantics differ, or only available through a standard library rather than the core language), — not present.

Notes on the partial (~) entries:

• Multiple supertypes for subtyping — Laurel's extending list lets a type declare several supertypes for is/as and subtyping. Java gets this from implementing multiple interfaces (and Python from its MRO). JavaScript has only a single prototype chain and no interface concept.

• Multiple implementation inheritance — this is the stronger form Python needs: inheriting fields and method implementations from several concrete parents, resolved by an MRO. Only Python has it fully; JavaScript relies on ad-hoc mixin patterns, and Java has none (interfaces provide default methods but no fields).

• Record types — an immutable aggregate compared by structural equality. Java has records directly. Python has @dataclass/NamedTuple (~, library/decorator-based). JavaScript has no record type (the Records & Tuples proposal is not shipped).

• Arbitrary-precision integers — only Python has them as the default int; Java and JavaScript expose them through a library (BigInteger, BigInt).

• Fixed-width bitvector operations — JavaScript's bitwise operators are 32-bit; Python integers are arbitrary width.

• do/while loops — Python has none.

• break / continue — Laurel does not yet have dedicated break/continue keywords (WIP). It already provides the more general primitive underneath them: a labelled block { … } L and an exit L statement that jumps to the end of that block. break is an exit of the block wrapping the loop, and continue an exit of the block wrapping the loop body, so the one primitive covers both. On the labelled-exit row, Python has break/continue without labels.

• Increment / decrement — Python has no such operators.

• Assignments in expression positions — Laurel allows assignments (and other imperative constructs) to appear where an expression is expected, and lifts them out into preceding statements. Java and JavaScript treat assignment as an expression directly. In Python assignments are statements; only the walrus operator := provides a restricted assignment expression.

• Algebraic datatypes / pattern matching — Java (sealed types + switch patterns) and Python (match) support a subset; JavaScript has none.

• Exceptions — Java has checked exceptions; JavaScript and Python have exceptions, but unchecked.

• C partial entries — C has raw pointers with manual malloc/free rather than managed reference objects (~), and structs are mutable aggregates without structural equality, so they are only a partial fit for record types (~). Casts exist but there is no runtime type test, so is/as is partial (~). Arbitrary-precision integers are library-only (for example GMP, ~), and strings are char arrays or standard-library routines rather than a first-class type (~). goto stands in for labelled loop exits (~), and generics are approximated with _Generic and macros (~). eval/dynamic code loading is available only indirectly through dlopen (~). C has no built-in sets or maps, no classes or inheritance, no exceptions, no reflection, and no garbage collection, so those rows are —.

• Implicit numeric widening — Java, Python, and C widen an integer to a floating-point value where one is expected (1 + 2.0). JavaScript has a single number type, so there is no integer to widen (—).

• Truthiness — Python, JavaScript, and C admit non-boolean values in boolean position, each with its own rule (0, "", empty containers, and null/None/undefined are false). Java rejects them: a condition must already be boolean (—).

• Dynamic type — Python and JavaScript are dynamically typed, so a value of any type flows into any variable. Java and C are statically typed with no such type (—).

Notes on the Core column. Core is Laurel's lowering target, a Boogie-style intermediate verification language, so the column records what survives to Core as a native construct rather than what a programmer writes. Core natively provides arbitrary-precision integers, reals, IEEE-754 floats, strings, maps (and sets as maps to bool), fixed-width bitvectors, while loops with invariants, algebraic datatypes with pattern matching, and parametric type constructors, so those rows are ✓. It has no object model — heap objects and reference equality are encoded through maps rather than being primitive (~), as are records (modelled with datatypes) and short-circuit operators (modelled with pure boolean operators). Everything Laurel lowers away before reaching Core is — : classes and inheritance, do/while, direct and labelled break/continue, increment/decrement, assignments in expression positions, procedures as values, exceptions, reflection, eval, shared-memory concurrency, and GC observability.

Notes on the not-planned (✗) entries. These are features that survive the source language's own compilation (they are not mere syntactic sugar) yet Laurel deliberately does not model, because they cannot be lowered into static Laurel constructs without either embedding a runtime interpreter or losing soundness, and they are fundamentally at odds with modular static verification.

• Reflection / runtime metaprogramming — all three source languages allow a program to inspect and rewrite its own structure at runtime: Java through java.lang.reflect and dynamic proxies, Python through getattr/setattr, __dict__ mutation, metaclasses, and monkey-patching, and JavaScript through Proxy/Reflect and prototype mutation (Object.setPrototypeOf). Laurel's static and flow-based typing, and its inference of composite types from a fixed set of assigned fields, assume the set of fields and methods of a type is known statically, so arbitrary self-modification is out of scope.

• eval / dynamic code loading — code that does not exist until runtime cannot be verified ahead of time. Python (eval/exec) and JavaScript (eval) have it directly; Java exposes it more indirectly through scripting and dynamic class loading (~).

• Garbage-collection observability — finalizers and weak references (Java finalize/WeakReference, Python __del__/weakref, JavaScript WeakRef/FinalizationRegistry) expose the nondeterministic timing of collection. Laurel models the heap abstractly and does not expose when, or whether, an object is collected.

Note on the shared-memory concurrency entry (WIP): Java has real shared-memory threads governed by the Java Memory Model (synchronized, volatile, happens-before); Python has threads under the GIL (✓); JavaScript is single-threaded and only achieves parallelism through workers that communicate by message passing (~). Laurel is currently sequential, and reasoning under a relaxed memory model is a large, separable piece of work, so this is planned rather than available.

1. 3.1. Proof-relevant subtyping
2. 3.2. Truthiness coercion
3. 3.3. Exceptions