Review and next steps

Tutorial Conclusion

You've learned to:

1. Write precise legal rules that capture obligations, conditions, and consequences

2. Model complex legal entities with proper types and relationships

3. Handle multi-step legal processes using the PROVISION approach

4. Organize complete regulatory schemes using the three-layer architecture

5. Understand the design principles that make L4 effective for legal modeling

6. Apply advanced techniques for real-world complexity

What's Next:

• Practice with your own legal domain (employment law, tax law, etc.)

• Experiment with the Jersey Charities Law model in the examples

• Explore integration with legal databases and case management systems

• Consider how L4 could improve legal drafting in your practice

Key Insight: L4 isn't just about automating existing legal processes—it's about thinking more clearly about how legal systems actually work, and designing better legal frameworks as a result.

---

Tutorial Reference

Basic Syntax

-- Comments start with --
IMPORT prelude                   -- Always start with this

-- Type definitions
DECLARE TypeName
    HAS field1 IS A Type1
        field2 IS A Type2

DECLARE EnumType IS ONE OF       -- Enumeration
    Option1
    Option2 HAS data IS A Type

-- Function definitions
GIVEN entity IS A Type           -- Input parameters
GIVETH A Type                    -- Return type
functionName MEANS expression    -- Function body

-- Contract definitions
GIVEN entity IS A Type
GIVETH A CONTRACT Actor Action
contractName MEANS
  PARTY Actor                    -- Who has the obligation
  MUST Action                    -- What they must do  
  WITHIN timeframe              -- Deadline (in days)
  HENCE FULFILLED               -- If they comply
  LEST FULFILLED                -- If they don't comply

Type Declarations

-- Basic record type
DECLARE Person
    HAS name IS A STRING
        age IS A NUMBER
        isActive IS A BOOLEAN

-- Enumeration with data
DECLARE Purpose IS ONE OF
    `prevention or relief of poverty`
    `advancement of education`
    otherPurpose HAS description IS A STRING

-- Actor/Action types for contracts
DECLARE Actor IS ONE OF
    PersonActor HAS person IS A Person
    OrganizationActor HAS name IS A STRING

DECLARE Action IS ONE OF
    FileDocument HAS content IS A STRING
    PayAmount HAS amount IS A NUMBER

PROVISION pattern

GIVEN entity IS A Type
GIVETH A PROVISION Actor Action
`contract name` MEANS
  IF condition                   -- Optional condition
  THEN PARTY ActorType parameter -- Actor with obligation
       MUST ActionType parameter -- Action they must perform
       WITHIN days               -- Time limit in days
       HENCE FULFILLED           -- Success outcome
       LEST FULFILLED            -- Failure outcome
  ELSE FULFILLED                 -- Alternative when condition false

Important:

• Always use proper Actor and Action constructors, not string literals

• Use simple parameters in MUST clauses - avoid complex object construction

• Parenthesize field access when used as function arguments: length (entity's field)

Value Creation

-- Simple values
DECIDE constantName IS value

-- Constructor with parameters (match exact field count)
DECIDE entityName IS TypeName field1Value field2Value field3Value

-- List construction
DECIDE listName IS LIST item1, item2, item3
DECIDE emptyList IS LIST  -- Empty list of inferred type

-- Date construction  
DECIDE dateValue IS Date 2024 6 15  -- year month day

Common Patterns

-- List operations (define length function first)
GIVEN a IS A TYPE
      list IS A LIST OF a
GIVETH A NUMBER
length list MEANS
  CONSIDER list
  WHEN EMPTY THEN 0
  WHEN x FOLLOWED BY xs THEN 1 + length xs

-- Boolean validation
GIVEN text IS A STRING
GIVETH A BOOLEAN
isNotEmpty MEANS NOT text EQUALS ""

-- List validation with quantifiers
GIVEN items IS A LIST OF Type
GIVETH A BOOLEAN
allValid MEANS all (GIVEN item YIELD condition) items

-- Field access in function arguments (always use parentheses)
length (entity's fieldName) > 0
elem item (entity's listField)
all (GIVEN x YIELD condition) (entity's items)

Essential Functions to Define

L4 is not done. It will continue to evolve and our prelude will expand. For the time being you can define your own imports to segregate out type definitions and helpful functions into seperate files.

-- e.g. Length function (not in prelude)
GIVEN a IS A TYPE
      list IS A LIST OF a
GIVETH A NUMBER
length list MEANS
  CONSIDER list
  WHEN EMPTY THEN 0
  WHEN x FOLLOWED BY xs THEN 1 + length xs

Taking L4 further

How to use L4 to compute financial contracts and obligations?

Checkout the example of a simple debt contract/promissory note.