+++
title = "Benefits of proofs by reflection"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b7"]
forwardlinks = []
zettelid = "3b7a"
+++

The two main benefits of proof by reflection are that:

-   The size of the proof is small, because the statement of the
    function is enough as a proof for it, meaning that it is often only
    linear in the size of the number being proven, for example.
-   Proofs by reflection also "just work", because the dependent type of
    the function gives a good indication about what proofs it will
    return. As it has been verified to be correct, one knows that the
    decision procedure will also work correctly. This is much better
    than defining a recursive `Ltac` function as that does not have any
    guarantees at all.