From 735b245871d94cb6ace8913cd1370b02b5aeb28b Mon Sep 17 00:00:00 2001 From: Leonardo Santiago Date: Sat, 1 Jun 2024 15:25:15 -0300 Subject: remove old theme, use bearblog theme instead --- .../posts/correctness-is-all-you-need/index.html | 750 --------------------- 1 file changed, 750 deletions(-) delete mode 100644 public/posts/correctness-is-all-you-need/index.html (limited to 'public/posts/correctness-is-all-you-need/index.html') diff --git a/public/posts/correctness-is-all-you-need/index.html b/public/posts/correctness-is-all-you-need/index.html deleted file mode 100644 index ae904b3..0000000 --- a/public/posts/correctness-is-all-you-need/index.html +++ /dev/null @@ -1,750 +0,0 @@ - - - - - - - - - - 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