Laurel Language Designer Guide

1. Design Goals🔗

Laurel is an intermediate analysis language that is designed to reduce the work required for analysing code from various languages. This page describes the sub-goals that Laurel has to achieve that higher goal. The remaining sections each focus on a sub-goal and describes the features that Laurel has to accompilsh it, why those features support that goal, and what alternative features were not added to the language and why. When evolving the language, this document must be updated to advocate for the changes. In particular, every language feature must be placed under a particular sub-goal.

Everything in this design guide is agnostic to how Laurel is implemented: we have tried to define Laurel without being influenced by its implementation, such as how it compiles to other languages.

Sub-goals:

  1. Enable proving both correctness and incorrectness properties of Laurel programs, through a combination of:

    1. Property based testing (PBT)

    2. Symbolic execution (aka verification), both bounded and unbounded

    3. Hybrid PBT and verification

    4. Data-flow analysis

    Laurel programs may contain constructs that are used by only some of these analyses.

  2. Make it cheap to target Laurel by adding to Laurel, the features that are shared between the languages that Laurel is compiled from. We expect source languages to reuse their existing compilers when possible, so language features that can be compiled away don't need to be considered. Right now Laurel is focussed on being a target for Java, Python, and JavaScript, but we expect that list to grow and it may also include non-GC'd languages such as C.

  3. Enable modular verification: every Laurel procedure can be verified independently.

  4. Minimize the amount of user code needed to enable verification. For example, Laurel never requires you to add a postcondition to a procedure.

  5. Enable finding proofs through an automated search. Laurel contains constructs that, when used correctly, help finding proofs. These features are still under design but think of a "proof by" construct that enables defining intermediate proof goals to guide the search.

  6. Use complete analysis algorithms to reduce the required proof effort. For example, we will use type inference to infer types when they are not statically known, and use those types to improve verification performance.

  7. Verification must be erasable. Removing verification code may not affect execution behavior. The reason for requiring verification code to be erasable is that we don't want to negatively effect the runtime performance of the program because we're verifying it - so we must be able to erase the verification code.

  8. Have a great user experience