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 --- content/posts/.#correctness-is-all-you-need.md | 1 - content/posts/correctness-is-all-you-need.md | 32 -------------------------- 2 files changed, 33 deletions(-) delete mode 120000 content/posts/.#correctness-is-all-you-need.md delete mode 100644 content/posts/correctness-is-all-you-need.md (limited to 'content/posts') diff --git a/content/posts/.#correctness-is-all-you-need.md b/content/posts/.#correctness-is-all-you-need.md deleted file mode 120000 index 0aea4a6..0000000 --- a/content/posts/.#correctness-is-all-you-need.md +++ /dev/null @@ -1 +0,0 @@ -leonardo@kunagisa.300940:1715192908 \ No newline at end of file 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 -- cgit v1.2.3