Laurel Language Designer Guide

Laurel Language Designer Guide

Table of Contents

1.	Design Goals
2.	Correctness checking features
3.	Prevent duplicate work
4.	Modular Verification
5.	Minimize Verification Code
6.	Automated proof search
7.	Use complete algorithms to reduce workload
8.	Verification code must be erasable
9.	Great user experience
10.	Planned features

10. Planned features

10.1.	Dynamic type
10.2.	Type inference
10.3.	Flow based types
10.4.	Global variables
10.5.	Non-determinism
10.6.	Immutable fields
10.7.	Reads clauses
10.8.	Frozen types
10.9.	Enhance support for transparent procedures
10.10.	Property-based testing
10.11.	Data-flow analysis
10.12.	Heap mutation in contracts
10.13.	Proof By
10.14.	Inference of composite types
10.15.	Decreases clauses
10.16.	Exception inference

10.9. Enhance support for transparent procedures

←10.8. Frozen types 10.10. Property-based testing→

10.9. Enhance support for transparent procedures🔗

Transparent procedures will support:

Destructive assignment
Multiple output parameters
Control flow with loops

←10.8. Frozen types 10.10. Property-based testing→