diff options
| author | Jakob L. Kreuze <zerodaysfordays@sdf.org> | 2024-08-05 16:31:01 -0400 |
|---|---|---|
| committer | Jakob L. Kreuze <zerodaysfordays@sdf.org> | 2024-08-05 16:31:01 -0400 |
| commit | 2a6edfb9341e510dfdc304772906e696064e08a2 (patch) | |
| tree | 37aefd071305905ce489aa6222c3f9507bbacd1b | |
| parent | 69c9162595a267425258e415b12ed472a9160b5e (diff) | |
[posts] Addendum addressing the issue Burkhardt Renz pointed out
| -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. |