3. Proofs🔗

Right now the only proofs in the Laurel implementation are termination proofs. We do not yet require any Laurel code to have more proofs than that. We are planning to define a semantics for Laurel in terms of Lean, and we will prove that the Laurel compilation passes preserve those semantics.