Add content

1 files changed, 19 insertions, 0 deletions

diff --git a/content/zettel/3d1.md b/content/zettel/3d1.md
new file mode 100644
index 0000000..ff0a159
--- /dev/null
+++ b/content/zettel/3d1.md
@@ -0,0 +1,19 @@
++++
+title = "Dafny"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3d"]
+forwardlinks = ["3d2"]
+zettelid = "3d1"
++++
+
+Dafny is a tool that was created by Runstan Lino, which is a language
+that was designed specifically for the purposes of verification. The
+main idea is that you can have preconditions and postconditions that
+describe the functionality of your program. These are then proven
+automatically by dafny, which uses the implementation to try and prove
+the postcondition assuming that the precondition holds.
+
+This cannot always be the case though, and one can therefore help the
+theorem prover by adding assertions in different places.