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
6.
Automated proof search
6.1.
Proof By
6.2.
Reads clauses
6.3.
Frozen types
←
5.4. Invoke on
6.1. Proof By
→
6. Automated proof search
🔗
Goal 5 was enabling the finding of proofs through automated search.
6.1.
Proof By
6.2.
Reads clauses
6.3.
Frozen types
←
5.4. Invoke on
6.1. Proof By
→