summaryrefslogtreecommitdiffhomepage
path: root/content/posts/correctness-is-all-you-need.md
diff options
context:
space:
mode:
authorLeonardo Santiago <[email protected]>2024-06-01 15:25:15 -0300
committerLeonardo Santiago <[email protected]>2024-06-01 15:25:15 -0300
commit735b245871d94cb6ace8913cd1370b02b5aeb28b (patch)
tree10d9e97d553a5059513a34a5f2b09ae8e9a0dab0 /content/posts/correctness-is-all-you-need.md
parent31bc6a2f54d86a4978be063f5e614881c625c597 (diff)
remove old theme, use bearblog theme instead
Diffstat (limited to 'content/posts/correctness-is-all-you-need.md')
-rw-r--r--content/posts/correctness-is-all-you-need.md32
1 files changed, 0 insertions, 32 deletions
diff --git a/content/posts/correctness-is-all-you-need.md b/content/posts/correctness-is-all-you-need.md
deleted file mode 100644
index 20ded9a..0000000
--- a/content/posts/correctness-is-all-you-need.md
+++ /dev/null
@@ -1,32 +0,0 @@
-+++
-title = "correctness is all you need"
-author = ["santi"]
-lastmod = 2024-05-09T23:35:32-03:00
-tags = ["coq", "rust"]
-draft = false
-+++
-
-```python
->>> 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:
-
-```python
->>> (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