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 +++++++++++++++++++ public/posts/index.html | 691 +++++++++++++++++ public/posts/index.xml | 22 + public/posts/page/1/index.html | 10 + public/posts/software-correctness/index.html | 821 +++++++++++++++++++++ 5 files changed, 2294 insertions(+) create mode 100644 public/posts/correctness-is-all-you-need/index.html create mode 100644 public/posts/index.html create mode 100644 public/posts/index.xml create mode 100644 public/posts/page/1/index.html create mode 100644 public/posts/software-correctness/index.html (limited to 'public/posts') 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 +

+ + +
+ + + + + + +
+ +
+ + + diff --git a/public/posts/index.html b/public/posts/index.html new file mode 100644 index 0000000..154bba7 --- /dev/null +++ b/public/posts/index.html @@ -0,0 +1,691 @@ + + + + + + + + + + posts · lowest case + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ ↓skip to main content +
+ + +
+ +
+ + +
+ + + + + + + + + + + + + + + +
+
+
+ + +
+
+ + + + + + + + +
+
+ + + +
+ +

posts

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

+ 2024 +

+ + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+ +
correctness is all you need
+ + + +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + ·1 min + + + + +
+ + + + + +
+ + + + + + + + + + + + + + + + coq + + + + + + + + rust + + + + + + + +
+ + + +
+ +
+ + + +
+ + + + + + + + + +
+ + + + +
+ + + +

+ © + 2024 + leonardo santiago +

+ + + + +

+ + + powered by Hugo & Blowfish +

+ + +
+ + + + + + +
+ +
+ + + diff --git a/public/posts/index.xml b/public/posts/index.xml new file mode 100644 index 0000000..104d58d --- /dev/null +++ b/public/posts/index.xml @@ -0,0 +1,22 @@ + + + + posts on lowest case + http://localhost:1313/posts/ + Recent content in posts on lowest case + Hugo -- gohugo.io + en + © 2024 leonardo santiago + Thu, 09 May 2024 23:35:32 -0300 + + correctness is all you need + http://localhost:1313/posts/correctness-is-all-you-need/ + Thu, 09 May 2024 23:35:32 -0300 + + http://localhost:1313/posts/correctness-is-all-you-need/ + >>> 0. + + + + + diff --git a/public/posts/page/1/index.html b/public/posts/page/1/index.html new file mode 100644 index 0000000..3e3304d --- /dev/null +++ b/public/posts/page/1/index.html @@ -0,0 +1,10 @@ + + + + http://localhost:1313/posts/ + + + + + + diff --git a/public/posts/software-correctness/index.html b/public/posts/software-correctness/index.html new file mode 100644 index 0000000..5a495c1 --- /dev/null +++ b/public/posts/software-correctness/index.html @@ -0,0 +1,821 @@ + + + + + + + + + + correctness is all you need · lowest case + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ ↓skip to main content +
+ + +
+ +
+ + +
+ + + + + + + + + + + + + + + +
+
+
+ + +
+
+ + + + + + + + +
+
+ + + +
+ + +
+ +
    + + + + + + + + + +
  1. + posts/ +
    2. + + + + +
+ + + +

+ correctness is all you need +

+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + ·1 min + + + + +
+ + + + + +
+ + + + + + + + + + + + + + + + coq + + + + + + + + rust + + + + + + + +
+ + + +
+ + + + + + + + + + + + + + + + + + + +
+ +
+ +
+
+ + +
+ + table of contents + +
+ +
+
+ +
+
+ + +
+ + + + +
+
+

you’re using the pythegorean theorem? that old unmaintained crap?

+
+

said no one, ever. the pythegorean theorem is treated as a mathematical foundation, that needs no questioning and that will always work. however, that couldn’t be more different from the way we treat modern software, ie. afraid of upgrading, avoiding unmaintained projects, and having to deal with constant breakage of upstream packages. why?

+ + +

taxonomy of bugs +
+ + + # + + +

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

+ © + 2024 + leonardo santiago +

+ + + + +

+ + + powered by Hugo & Blowfish +

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