diff options
Diffstat (limited to 'posts')
| -rw-r--r-- | posts/what-ive-learned-about-formal-methods.org | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/posts/what-ive-learned-about-formal-methods.org b/posts/what-ive-learned-about-formal-methods.org index ca32956..e5b0873 100644 --- a/posts/what-ive-learned-about-formal-methods.org +++ b/posts/what-ive-learned-about-formal-methods.org @@ -728,7 +728,7 @@ Compared to SMT, proof assistants tend to be far less restrictive on the kinds o ** Specification -When we wrote our property tests for Scheme, we formalized our properties as Scheme functions returning booleans (predicates). We did something similar when we wrote our Forge/Alloy predicates as well. I've found that there are (broadly speaking) two approaches to the concept when it comes to proof assistants. One approach is to retain _decidability_ as much as possible and write predicates as boolean returning functions -- for example: +When we wrote our property tests for Scheme, we formalized our properties as Scheme functions returning booleans (predicates). We did something similar when we wrote our Forge/Alloy predicates as well. I've found that there are (broadly speaking) two approaches to the concept when it comes to proof assistants. One approach is to retain _decidability_ as much as possible and write predicates as boolean returning functions -- for example:[fn:13] #+BEGIN_SRC lean4 def sorted : List Nat → Bool := @@ -2116,3 +2116,5 @@ to my =init.el= and I get a goal buffer similar to the old lean-mode or Proof Ge [fn:11] Even so, I'm covering only a small part of the problem, so I wouldn't expect this article to be that useful to someone trying to cheese a homework assignment. [fn:12] For more realistic examples of property testing in Scheme, see [[https://ngyro.com/software/guile-quickcheck.html][guile-quickcheck]]. + +[fn:13] Addendum on August 5th, 2024: Burkhardt Renz pointed out in the comments section that this definition is subtly incorrect. Example: =sorted [1, 2, 1]= evaluates to =true=. Rather than =(sorted xs)=, it should be =(sorted (List.cons x₂ xs))=. This is a good example of where formal methods can fail - if your specification is faulty, then the rest falls apart. |