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 --- content/posts/.#correctness-is-all-you-need.md | 1 + content/posts/correctness-is-all-you-need.md | 32 ++++++++++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 120000 content/posts/.#correctness-is-all-you-need.md create 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 new file mode 120000 index 0000000..0aea4a6 --- /dev/null +++ b/content/posts/.#correctness-is-all-you-need.md @@ -0,0 +1 @@ +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 new file mode 100644 index 0000000..20ded9a --- /dev/null +++ b/content/posts/correctness-is-all-you-need.md @@ -0,0 +1,32 @@ ++++ +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