l4-computational-law

L4 with IDE

L4 is a domain-specific programming language for law, designed to bring software engineering rigor to legal drafting and contract analysis. Just as programmers have powerful IDEs, compilers, debuggers, and test suites, L4 provides legal professionals with a comprehensive toolchain for creating precise, unambiguous, and verifiable legal specifications.

What is L4?

L4 treats legal rules and contracts as executable specifications rather than documents. Drawing from logic programming, functional programming, temporal logic, and formal verification, L4 allows you to:

• Formalize legal rules with mathematical precision
• Test contracts against scenarios before deployment
• Find logical contradictions and loopholes automatically
• Generate user-facing web applications from legal specifications
• Explain decisions with audit-grade evaluation traces
• Integrate with enterprise systems via REST APIs

This repository includes the L4 compiler toolchain, IDE extensions for Visual Studio Code, an interactive REPL, a web-based editor, visualization tools, and a decision service for runtime evaluation.

What Can You Do With L4?

"After I convert my rules to L4, what can I usefully do with them?"

From a single L4 source file, you automatically get:

• 🌐 REST APIs — Expose functions as HTTP endpoints with @export annotation
• 🤖 AI Tool Integration — MCP server for Claude, Cursor, VS Code Copilot; WebMCP for browser AI agents
• 📂 Source Code Browsing — REST API and MCP tools to search, read, and explore deployed L4 files
• 🧙 Web Applications — Auto-generated questionnaires with smart question ordering
• 📊 Interactive Visualizations — Ladder diagrams and evaluation traces
• 🧪 Test Suites — Automated testing with golden files and assertions
• 📚 Documentation — OpenAPI 3.0 specs, JSON schemas, and type definitions
• 🔗 Enterprise Integration — JSON/REST bridges to existing systems

See doc/MARKETECTURE.md for the complete "whole product" picture of what L4 enables.

Real-World Impact

L4 has been piloted with organizations in both public and private sectors:

• Government Regulatory Compliance: Encoded secondary legislation to auto-generate web wizards that explain legal obligations to citizens. Formal verification discovered a race condition—a double bind where contradictory clauses could require and prohibit the same action simultaneously.

• Insurance Policy Analysis: Formalized insurance contracts from major global providers, discovering ambiguities in payout formulas that potentially caused millions of dollars in claims leakage.

• Legislative Drafting: Working with government legal drafting offices on rules-as-code initiatives, enabling legislation to be written in machine-verifiable form from the start.

• Commercial Agreements: Transformed complex fee schedules and payment terms into L4, serving them via SQL-like APIs for enterprise system integration.

Documentation

For Developers

• doc/dev/setup.md - Complete developer setup guide for Haskell and TypeScript development
• doc/dev/local-config.md - Local development guide (running with cabal)
• dev-start.sh - Helper script for starting services locally

For DevOps

• doc/dev/deployment/provisioning.md - Setting up new servers from scratch (nixos-anywhere)
• doc/dev/deployment/deployment.md - Deploying to existing dev/prod servers
• nix/README.md - NixOS configuration reference

Gallery

Syntax Highlighting for Boolean-oriented decision logic

Decision Logic Visualization as a ladder diagram circuit

Trace Visualization

Curious how an L4 decision actually unfolded? Every tool in this repo can show you the evaluation trace as a GraphViz diagram:

• CLI: jl4-cli --graphviz myfile.l4 > trace.dot, then render with dot -Tsvg trace.dot > trace.svg.
• REPL: Load a file, run :trace your expression, or turn on :tracefile traces/session to capture numbered .dot files with timestamps, imports, and the final result right in the header.
• Decision Service: Call POST /deployments/{id}/functions/{fn}/evaluation?trace=full&graphviz=true to get a graphviz object containing the DOT source. Batch requests set graphviz=true to attach an @graphviz blob per case.

These traces act like explainability receipts for deterministic logic: you can follow each node from the top-level question down to the exact condition or branch that determined the answer. Install GraphViz (brew install graphviz or apt-get install graphviz) to unlock the PNG/SVG outputs.

Trace Logging