Julia reference implementation of the PolyglotFormalisms Common Library with formal verification.
PolyglotFormalisms.jl provides formally verified implementations of the minimal overlap functions specified in the aggregate-library project. This package serves as a Julia reference implementation for cross-language semantic equivalence verification.
The aggregate-library defines a minimal intersection of functionality across radically different programming languages. PolyglotFormalisms.jl adds value by:
Formal Verification — Mathematical properties are proven using Axiom.jl’s
@provemacro (planned)Reference Implementation — Serves as a semantically verified baseline for other language implementations
Conformance Testing — Test suite exactly matches PolyglotFormalisms specifications
Cross-Language Bridge — Enables verification that ReScript, Gleam, Elixir implementations satisfy the same properties
using PolyglotFormalisms
# Arithmetic operations
Arithmetic.add(2, 3) # 5
Arithmetic.subtract(10, 3) # 7
Arithmetic.multiply(4, 5) # 20
Arithmetic.divide(10, 2) # 5.0
Arithmetic.modulo(10, 3) # 1# Comparison operations
Comparison.less_than(2, 3) # true
Comparison.equal(5, 5) # true# Collection operations
Collection.map_items(x -> x^2, [1, 2, 3]) # [1, 4, 9]
Collection.filter_items(iseven, [1, 2, 3, 4]) # [2, 4]
Collection.fold_items(+, 0, [1, 2, 3]) # 6# Conditional operations
Conditional.if_then_else(true, "yes", "no") # "yes"
Conditional.coalesce(nothing, nothing, 42) # 42
Conditional.clamp_value(15, 0, 10) # 10| Function | Description |
|---|---|
| Sum of two numbers |
| Difference of two numbers |
| Product of two numbers |
| Quotient of two numbers |
| Remainder of division |
Verified properties: commutativity, associativity, identity, zero element, distributivity.
| Function | Description |
|---|---|
| a < b |
| a > b |
| a == b |
| a != b |
| a ⇐ b |
| a >= b |
Verified properties: trichotomy, transitivity, reflexivity (for equal, less_equal, greater_equal), antisymmetry.
| Function | Description |
|---|---|
| Logical conjunction |
| Logical disjunction |
| Logical negation |
Verified properties: commutativity, associativity, identity, De Morgan’s laws, double negation, excluded middle.
| Function | Description |
|---|---|
| Concatenate two strings |
| String length |
| Extract substring |
| Find first occurrence (0 if not found) |
| Check if string contains substring |
| Check prefix |
| Check suffix |
| Convert to uppercase |
| Convert to lowercase |
| Remove leading/trailing whitespace |
| Split string by delimiter |
| Join strings with separator |
| Replace occurrences of substring |
| Check if string is empty |
Verified properties: concat associativity, concat identity, length non-negativity, split/join roundtrip, trim idempotence.
| Function | Description |
|---|---|
| Apply function to each element |
| Keep elements matching predicate |
| Left-fold with accumulator |
| Pair elements positionally |
| Map and flatten results |
| Group elements by key function |
| Stable sort by comparison function |
| Remove duplicates (preserve order) |
| Split into (matching, non-matching) |
| Take first n elements |
| Drop first n elements |
| True if any element matches |
| True if all elements match |
Verified properties: functor identity (map id = id), functor composition, filter/partition consistency, fold universality, take/drop complementarity, De Morgan duality (any/all).
| Function | Description |
|---|---|
| Total ternary conditional |
| Conditional value ( |
| Inverse conditional value |
| First non-nothing value |
| Clamp number to range [lo, hi] |
Verified properties: if_then_else totality, when/unless duality, coalesce idempotence, clamp boundary conditions, clamp idempotence within range.
Test suite exactly matches the PolyglotFormalisms specification test cases:
using Test
using PolyglotFormalisms
@testset"PolyglotFormalisms Conformance"begin# Test cases from specs/arithmetic/add.md@test Arithmetic.add(2, 3) ==5@test Arithmetic.add(-5, 3) ==-2@test Arithmetic.add(0, 0) ==0@test Arithmetic.add(1.5, 2.5) ==4.0@test Arithmetic.add(-10, -20) ==-30# Property verification@test Arithmetic.add(5, 3) == Arithmetic.add(3, 5) # Commutativity@test Arithmetic.add(Arithmetic.add(2, 3), 4) == Arithmetic.add(2, Arithmetic.add(3, 4)) # AssociativityendRun full test suite:
julia --project=. -e 'using Pkg; Pkg.test()'When Axiom.jl is available as a dependency, formal proofs will be automatically verified at compile time:
# Future integration:@proveforall(a, b) doadd(a, b) ==add(b, a) end@proveforall(a, b, c) doadd(add(a, b), c) ==add(a, add(b, c)) end@proveforall(a) doadd(a, 0) == a endThis enables:
Compile-time verification of mathematical properties
Automatic error detection if implementations violate proven properties
Formal certificates proving correctness for safety-critical applications
PolyglotFormalisms.jl serves as a formally verified reference for semantic equivalence checking:
Implement in target language (ReScript, Gleam, Elixir)
Run PolyglotFormalisms conformance tests in both languages
Use Axiom.jl + SMTLib.jl to prove semantic equivalence
Generate verification certificate
using PolyglotFormalisms
using Axiom
using SMTLib
# Verify ReScript implementation semantically equivalent to Juliaverify_equivalence(
julia_impl = Arithmetic.add,
rescript_impl = RescriptFFI.add,
properties = [commutativity, associativity, identity]
)Current: 6 modules implemented, 422 passing tests.
| Module | Operations | Status |
|---|---|---|
Arithmetic | 5 | Complete |
Comparison | 6 | Complete |
Logical | 3 | Complete |
StringOps | 14 | Complete |
Collection | 13 | Complete |
Conditional | 5 | Complete |
Planned: Axiom.jl integration for compile-time formal proofs.
Minimal intersection — Only functions that work across all target languages
Clear semantics — Unambiguous behavioral specifications
Testable — Executable test cases for every operation
Provable — Mathematical properties verified with formal methods
Extensible — Each ecosystem extends through its standard library
Pierce, B.C. Types and Programming Languages. MIT Press, 2002.
Winskel, G. The Formal Semantics of Programming Languages. MIT Press, 1993.
Mac Lane, S. Categories for the Working Mathematician. 2nd ed., Springer, 1998.
Wadler, P. "Theorems for free!" FPCA '89, ACM, 1989.
IEEE 754-2019. IEEE Standard for Floating-Point Arithmetic. IEEE, 2019.
See TOPOLOGY.md for a visual architecture map and completion dashboard.
aggregate-library — PolyglotFormalisms specification
alib-for-rescript — ReScript implementation
polyglot-formalisms-gleam — Gleam implementation
polyglot-formalisms-elixir — Elixir implementation
Axiom.jl — Formal verification for ML models
Wondering how this works? See EXPLAINME.adoc.
SPDX-License-Identifier: CC-BY-SA-4.0
See LICENSE.