4 files changed, 58 insertions, 0 deletions
diff --git a/content/about/index.md b/content/about/index.md
new file mode 100644
index 0000000..831e9ec
--- /dev/null
+++ b/content/about/index.md
@@ -0,0 +1,15 @@
++++
+title = "about"
+author = ["santi"]
+lastmod = 2024-05-01T11:53:23-03:00
+draft = false
++++
+
+i'm leonardo santiago, a software engineer based in brazil. my interests are in compiler design, programming tools (emacs) and functional programming, usually dabbliing in related topics too. i'm most confortable in nix and rust, but i know a fair share of other languages.
+
+currently, software engineer @ [Mixrank](https://mixrank.com).
+
+this blog was built using [hugo](https://github.com/gohugoio/hugo), and it's source code is openly available here:
+{{< github repo="o-santi/nixos" >}}
+
+you can find me at: [{{< icon "email" >}}](mailto:[email protected]) [{{< icon "linkedin" >}}](https://www.linkedin.com/in/leonardo-ribeiro-santiago/) [{{< icon "github" >}}](https://github.com/o-santi) [{{< icon "telegram" >}}](https://t.me/osanti4) [{{< icon "twitter" >}}](https://twitter.com/o_santi_)
diff --git a/content/index.md b/content/index.md
new file mode 100644
index 0000000..9e4122e
--- /dev/null
+++ b/content/index.md
@@ -0,0 +1,10 @@
++++
+title = "lowest case"
+author = ["santi"]
+lastmod = 2024-05-01T11:53:23-03:00
+draft = false
++++
+
+a lower case only blog, purely for aesthetics.
+
+here I talk about discrete mathematics (mostly computer science), including compilers, language theory, type theory, computability theory, software correctness, formal verification, and any other (entirely theoretical almost non-applicable) nerd topic you can think of.
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 @@
+[email protected]: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