diff options
Diffstat (limited to 'content/zettel/3b7a.md')
| -rw-r--r-- | content/zettel/3b7a.md | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/content/zettel/3b7a.md b/content/zettel/3b7a.md new file mode 100644 index 0000000..af90b26 --- /dev/null +++ b/content/zettel/3b7a.md @@ -0,0 +1,21 @@ ++++ +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. |