From 31bc6a2f54d86a4978be063f5e614881c625c597 Mon Sep 17 00:00:00 2001 From: Leonardo Santiago Date: Wed, 29 May 2024 08:44:12 -0300 Subject: new blog using hugo again --- .../posts/correctness-is-all-you-need/index.html | 750 +++++++++++++++++++++ 1 file changed, 750 insertions(+) create mode 100644 public/posts/correctness-is-all-you-need/index.html (limited to 'public/posts/correctness-is-all-you-need') diff --git a/public/posts/correctness-is-all-you-need/index.html b/public/posts/correctness-is-all-you-need/index.html new file mode 100644 index 0000000..ae904b3 --- /dev/null +++ b/public/posts/correctness-is-all-you-need/index.html @@ -0,0 +1,750 @@ + + + + + + + + + + correctness is all you need · lowest case + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ ↓skip to main content +
+ + +
+ +
+ + +
+ + + + + + + + + + + + + + + +
+
+
+ + +
+
+ + + + + + + + +
+
+ + + +
+ + +
+ +
    + + + + + + + + + +
  1. + posts/ +
    2. + + + + +
+ + + +

+ correctness is all you need +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + ·1 min + + + + +
+ + + + + +
+ + + + + + + + + + + + + + + + coq + + + + + + + + rust + + + + + + + +
+ + + +
+ + + + + + + + + + + + + + + + + + + +
+ +
+ + + +
+ + + + +
+ 
>>> 0.1 + 0.2
+0.30000000000000004
+

which of course is an annoying encounter for the unitiated in floats, but there’s a much bigger problem, that usually isn’t noticed at all until much later, that float addition itself isn’t even associative:

+
>>> (0.1 + 0.2) + 0.3
+0.6000000000000001
+>>> 0.1 + (0.2 + 0.3)
+0.6
+>>> 0.1 + (0.2 + 0.3) == (0.1 + 0.2) + 0.3
+False
+>>>
+

and this is a problem, because associativity is a big underlying assumption that we commonly have for numbers, when, for example, summing a list in reverse. other common pitfalls include:

+
    +
  • not all numbers have an additive inverse, ie. for some number n, n + (-n) != n.
    • +
  • not all numbers different than 0 have a multiplicative inverse, ie. for some number n, n / n != 1.
    • +
  • addition is not commutative, ie. for numbers a b, a + b != b + a.
    • +
+

and the list goes you on, you get the idea. this usually isn’t thought of the main problems in

+ +
+ + + + + + + +
+ + + + + + + + + + + + + + +
+
+ + + + + + +
+
+ + +
+ + + + +
+ + + +

+ © + 2024 + leonardo santiago +

+ + + + +

+ + + powered by Hugo & Blowfish +

+ + +
+ + + + + + +
+ +
+ + + -- cgit v1.2.3