summaryrefslogtreecommitdiffhomepage
path: root/public/posts/correctness-is-all-you-need/index.html
diff options
context:
space:
mode:
authorLeonardo Santiago <[email protected]>2024-05-29 08:44:12 -0300
committerLeonardo Santiago <[email protected]>2024-05-29 08:44:12 -0300
commit31bc6a2f54d86a4978be063f5e614881c625c597 (patch)
tree5e79ef2c765b395d4e4a74ff45a7af09eee0d38c /public/posts/correctness-is-all-you-need/index.html
new blog using hugo again
Diffstat (limited to 'public/posts/correctness-is-all-you-need/index.html')
-rw-r--r--public/posts/correctness-is-all-you-need/index.html750
1 files changed, 750 insertions, 0 deletions
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 @@
+<!DOCTYPE html>
+<html lang="en" dir="ltr" class="scroll-smooth" data-default-appearance="dark"
+ data-auto-appearance="true"><head><script src="/livereload.js?mindelay=10&amp;v=2&amp;port=1313&amp;path=livereload" data-no-instant defer></script>
+ <meta charset="utf-8" />
+
+ <meta http-equiv="content-language" content="en" />
+
+ <meta name="viewport" content="width=device-width, initial-scale=1.0" />
+ <meta http-equiv="X-UA-Compatible" content="ie=edge" />
+
+ <title>correctness is all you need &middot; lowest case</title>
+ <meta name="title" content="correctness is all you need &middot; lowest case" />
+
+
+ <meta name="keywords" content="coq, rust, " />
+
+
+ <link rel="canonical" href="http://localhost:1313/posts/correctness-is-all-you-need/" />
+
+
+
+
+
+
+
+
+
+
+ <link type="text/css" rel="stylesheet" href="/css/main.bundle.min.81c7ce66608dd0b86aa3e571076f8794993d50f0d4a5b153013edfc28642a93c4104edfdc604558908c3624b8e99386757d81f1bf8c4452c6220cf4c63970408.css"
+ integrity="sha512-gcfOZmCN0Lhqo&#43;VxB2&#43;HlJk9UPDUpbFTAT7fwoZCqTxBBO39xgRViQjDYkuOmThnV9gfG/jERSxiIM9MY5cECA==" />
+
+
+ <script type="text/javascript" src="/js/appearance.min.516a16745bea5a9bd011138d254cc0fd3973cd55ce6e15f3dec763e7c7c2c7448f8fe7b54cca811cb821b0c7e12cd161caace1dd794ac3d34d40937cbcc9ee12.js"
+ integrity="sha512-UWoWdFvqWpvQERONJUzA/TlzzVXObhXz3sdj58fCx0SPj&#43;e1TMqBHLghsMfhLNFhyqzh3XlKw9NNQJN8vMnuEg=="></script>
+
+
+
+
+
+
+
+
+
+ <script defer type="text/javascript" id="script-bundle" src="/js/main.bundle.min.b36dda9ec4ec11e967fd341e7d57b8c484ac7a39f8f329f7bcf7ce4812569de8607db866a086d4789956ac0b74967e251c9a566d94d469dd28b8787fed4f46f5.js"
+ integrity="sha512-s23ansTsEeln/TQefVe4xISsejn48yn3vPfOSBJWnehgfbhmoIbUeJlWrAt0ln4lHJpWbZTUad0ouHh/7U9G9Q==" data-copy="" data-copied=""></script>
+
+
+ <script src="/js/zoom.min.js"></script>
+
+
+
+ <link rel="apple-touch-icon" sizes="180x180" href="/apple-touch-icon.png" />
+ <link rel="icon" type="image/png" sizes="32x32" href="/favicon-32x32.png" />
+ <link rel="icon" type="image/png" sizes="16x16" href="/favicon-16x16.png" />
+ <link rel="manifest" href="/site.webmanifest" />
+
+
+
+
+
+
+
+ <meta property="og:url" content="http://localhost:1313/posts/correctness-is-all-you-need/">
+ <meta property="og:site_name" content="lowest case">
+ <meta property="og:title" content="correctness is all you need">
+ <meta property="og:description" content="&amp;gt;&amp;gt;&amp;gt; 0.">
+ <meta property="og:locale" content="en">
+ <meta property="og:type" content="article">
+ <meta property="article:section" content="posts">
+ <meta property="article:published_time" content="2024-05-09T23:35:32-03:00">
+ <meta property="article:modified_time" content="2024-05-09T23:35:32-03:00">
+ <meta property="article:tag" content="coq">
+ <meta property="article:tag" content="rust">
+
+ <meta name="twitter:card" content="summary"><meta name="twitter:title" content="correctness is all you need">
+<meta name="twitter:description" content="&gt;&gt;&gt; 0.">
+
+
+ <script type="application/ld+json">
+ [{
+ "@context": "https://schema.org",
+ "@type": "Article",
+ "articleSection": "posts",
+ "name": "correctness is all you need",
+ "headline": "correctness is all you need",
+
+ "abstract": "\u0026gt;\u0026gt;\u0026gt; 0.",
+ "inLanguage": "en",
+ "url" : "http:\/\/localhost:1313\/posts\/correctness-is-all-you-need\/",
+ "author" : {
+ "@type": "Person",
+ "name": "leonardo santiago"
+ },
+ "copyrightYear": "2024",
+ "dateCreated": "2024-05-09T23:35:32-03:00",
+ "datePublished": "2024-05-09T23:35:32-03:00",
+
+ "dateModified": "2024-05-09T23:35:32-03:00",
+
+ "keywords": ["coq","rust"],
+
+ "mainEntityOfPage": "true",
+ "wordCount": "169"
+ }]
+ </script>
+
+
+
+
+ <meta name="author" content="leonardo santiago" />
+
+
+
+ <link href="mailto:[email protected]" rel="me" />
+
+
+ <link href="https://github.com/o-santi" rel="me" />
+
+
+ <link href="https://gitlab.com/o-santi" rel="me" />
+
+
+ <link href="https://www.linkedin.com/in/leonardo-ribeiro-santiago/" rel="me" />
+
+
+ <link href="https://t.me/osanti4" rel="me" />
+
+
+ <link href="https://twitter.com/o-santi" rel="me" />
+
+
+
+
+
+<script src="/lib/jquery/jquery.slim.min.js" integrity=""></script>
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ <meta name="theme-color"/>
+
+
+</head>
+<body
+ class="flex flex-col h-screen px-6 m-auto text-lg leading-7 max-w-7xl bg-neutral text-neutral-900 dark:bg-neutral-800 dark:text-neutral sm:px-14 md:px-24 lg:px-32">
+ <div id="the-top" class="absolute flex self-center">
+ <a class="px-3 py-1 text-sm -translate-y-8 rounded-b-lg bg-primary-200 focus:translate-y-0 dark:bg-neutral-600"
+ href="#main-content"><span
+ class="font-bold text-primary-600 ltr:pr-2 rtl:pl-2 dark:text-primary-400">&darr;</span>skip to main content</a>
+ </div>
+
+
+ <div style="padding-left:0;padding-right:0;padding-top:2px;padding-bottom:3px"
+ class="main-menu flex items-center justify-between px-4 py-6 sm:px-6 md:justify-start space-x-3">
+
+ <div class="flex flex-1 items-center justify-between">
+ <nav class="flex space-x-3">
+
+
+ <a href="/" class="text-base font-medium text-gray-500 hover:text-gray-900">lowest case</a>
+
+
+ </nav>
+ <nav class="hidden md:flex items-center space-x-5 md:ml-12 h-12">
+
+
+
+
+ <a href="" class="flex items-center text-gray-500 hover:text-primary-600 dark:hover:text-primary-400">
+
+ <p class="text-base font-medium" title="">
+ about
+ </p>
+</a>
+
+
+
+
+ <a href="/posts/" class="flex items-center text-gray-500 hover:text-primary-600 dark:hover:text-primary-400">
+
+ <p class="text-base font-medium" title="">
+ blog
+ </p>
+</a>
+
+
+
+
+ <a href="/tags/" class="flex items-center text-gray-500 hover:text-primary-600 dark:hover:text-primary-400">
+
+ <p class="text-base font-medium" title="">
+ tags
+ </p>
+</a>
+
+
+
+
+
+
+
+
+
+ <button id="search-button" aria-label="Search" class="text-base hover:text-primary-600 dark:hover:text-primary-400"
+ title="">
+
+
+ <span class="relative block icon">
+ <svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="search" class="svg-inline--fa fa-search fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M505 442.7L405.3 343c-4.5-4.5-10.6-7-17-7H372c27.6-35.3 44-79.7 44-128C416 93.1 322.9 0 208 0S0 93.1 0 208s93.1 208 208 208c48.3 0 92.7-16.4 128-44v16.3c0 6.4 2.5 12.5 7 17l99.7 99.7c9.4 9.4 24.6 9.4 33.9 0l28.3-28.3c9.4-9.4 9.4-24.6.1-34zM208 336c-70.7 0-128-57.2-128-128 0-70.7 57.2-128 128-128 70.7 0 128 57.2 128 128 0 70.7-57.2 128-128 128z"/></svg>
+
+ </span>
+
+
+ </button>
+
+
+
+
+
+ <div
+ class="ltr:mr-14 rtl:ml-14 flex items-center">
+ <button id="appearance-switcher" aria-label="Dark mode switcher" type="button" class="text-base hover:text-primary-600 dark:hover:text-primary-400">
+ <div class="flex items-center justify-center dark:hidden">
+
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M32 256c0-123.8 100.3-224 223.8-224c11.36 0 29.7 1.668 40.9 3.746c9.616 1.777 11.75 14.63 3.279 19.44C245 86.5 211.2 144.6 211.2 207.8c0 109.7 99.71 193 208.3 172.3c9.561-1.805 16.28 9.324 10.11 16.95C387.9 448.6 324.8 480 255.8 480C132.1 480 32 379.6 32 256z"/></svg>
+
+ </span>
+
+
+ </div>
+ <div class="items-center justify-center hidden dark:flex">
+
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M256 159.1c-53.02 0-95.1 42.98-95.1 95.1S202.1 351.1 256 351.1s95.1-42.98 95.1-95.1S309 159.1 256 159.1zM509.3 347L446.1 255.1l63.15-91.01c6.332-9.125 1.104-21.74-9.826-23.72l-109-19.7l-19.7-109c-1.975-10.93-14.59-16.16-23.72-9.824L256 65.89L164.1 2.736c-9.125-6.332-21.74-1.107-23.72 9.824L121.6 121.6L12.56 141.3C1.633 143.2-3.596 155.9 2.736 164.1L65.89 256l-63.15 91.01c-6.332 9.125-1.105 21.74 9.824 23.72l109 19.7l19.7 109c1.975 10.93 14.59 16.16 23.72 9.824L256 446.1l91.01 63.15c9.127 6.334 21.75 1.107 23.72-9.822l19.7-109l109-19.7C510.4 368.8 515.6 356.1 509.3 347zM256 383.1c-70.69 0-127.1-57.31-127.1-127.1c0-70.69 57.31-127.1 127.1-127.1s127.1 57.3 127.1 127.1C383.1 326.7 326.7 383.1 256 383.1z"/></svg>
+
+ </span>
+
+
+ </div>
+ </button>
+ </div>
+
+
+ </nav>
+ <div class="flex md:hidden items-center space-x-5 md:ml-12 h-12">
+
+ <span></span>
+
+
+
+
+
+ <button id="search-button-mobile" aria-label="Search" class="text-base hover:text-primary-600 dark:hover:text-primary-400"
+ title="">
+
+
+ <span class="relative block icon">
+ <svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="search" class="svg-inline--fa fa-search fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M505 442.7L405.3 343c-4.5-4.5-10.6-7-17-7H372c27.6-35.3 44-79.7 44-128C416 93.1 322.9 0 208 0S0 93.1 0 208s93.1 208 208 208c48.3 0 92.7-16.4 128-44v16.3c0 6.4 2.5 12.5 7 17l99.7 99.7c9.4 9.4 24.6 9.4 33.9 0l28.3-28.3c9.4-9.4 9.4-24.6.1-34zM208 336c-70.7 0-128-57.2-128-128 0-70.7 57.2-128 128-128 70.7 0 128 57.2 128 128 0 70.7-57.2 128-128 128z"/></svg>
+
+ </span>
+
+
+ </button>
+
+
+
+
+ <button id="appearance-switcher-mobile" aria-label="Dark mode switcher" type="button" class="text-base hover:text-primary-600 dark:hover:text-primary-400" style="margin-right:5px">
+ <div class="flex items-center justify-center dark:hidden">
+
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M32 256c0-123.8 100.3-224 223.8-224c11.36 0 29.7 1.668 40.9 3.746c9.616 1.777 11.75 14.63 3.279 19.44C245 86.5 211.2 144.6 211.2 207.8c0 109.7 99.71 193 208.3 172.3c9.561-1.805 16.28 9.324 10.11 16.95C387.9 448.6 324.8 480 255.8 480C132.1 480 32 379.6 32 256z"/></svg>
+
+ </span>
+
+
+ </div>
+ <div class="items-center justify-center hidden dark:flex">
+
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M256 159.1c-53.02 0-95.1 42.98-95.1 95.1S202.1 351.1 256 351.1s95.1-42.98 95.1-95.1S309 159.1 256 159.1zM509.3 347L446.1 255.1l63.15-91.01c6.332-9.125 1.104-21.74-9.826-23.72l-109-19.7l-19.7-109c-1.975-10.93-14.59-16.16-23.72-9.824L256 65.89L164.1 2.736c-9.125-6.332-21.74-1.107-23.72 9.824L121.6 121.6L12.56 141.3C1.633 143.2-3.596 155.9 2.736 164.1L65.89 256l-63.15 91.01c-6.332 9.125-1.105 21.74 9.824 23.72l109 19.7l19.7 109c1.975 10.93 14.59 16.16 23.72 9.824L256 446.1l91.01 63.15c9.127 6.334 21.75 1.107 23.72-9.822l19.7-109l109-19.7C510.4 368.8 515.6 356.1 509.3 347zM256 383.1c-70.69 0-127.1-57.31-127.1-127.1c0-70.69 57.31-127.1 127.1-127.1s127.1 57.3 127.1 127.1C383.1 326.7 326.7 383.1 256 383.1z"/></svg>
+
+ </span>
+
+
+ </div>
+ </button>
+
+
+ </div>
+ </div>
+ <div class="-my-2 -mr-2 md:hidden">
+
+ <label id="menu-button" for="menu-controller" class="block">
+ <input type="checkbox" id="menu-controller" class="hidden" />
+
+ <div class="cursor-pointer hover:text-primary-600 dark:hover:text-primary-400">
+
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 448 512"><path fill="currentColor" d="M0 96C0 78.33 14.33 64 32 64H416C433.7 64 448 78.33 448 96C448 113.7 433.7 128 416 128H32C14.33 128 0 113.7 0 96zM0 256C0 238.3 14.33 224 32 224H416C433.7 224 448 238.3 448 256C448 273.7 433.7 288 416 288H32C14.33 288 0 273.7 0 256zM416 448H32C14.33 448 0 433.7 0 416C0 398.3 14.33 384 32 384H416C433.7 384 448 398.3 448 416C448 433.7 433.7 448 416 448z"/></svg>
+
+ </span>
+
+
+ </div>
+ <div id="menu-wrapper" style="padding-top:5px;"
+ class="fixed inset-0 z-30 invisible w-screen h-screen m-0 overflow-auto transition-opacity opacity-0 cursor-default bg-neutral-100/50 backdrop-blur-sm dark:bg-neutral-900/50">
+ <ul
+ class="flex space-y-2 mt-3 flex-col items-end w-full px-6 py-6 mx-auto overflow-visible list-none ltr:text-right rtl:text-left max-w-7xl">
+
+ <li>
+ <span
+ class="cursor-pointer inline-block align-text-bottom hover:text-primary-600 dark:hover:text-primary-400">
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 320 512"><path fill="currentColor" d="M310.6 361.4c12.5 12.5 12.5 32.75 0 45.25C304.4 412.9 296.2 416 288 416s-16.38-3.125-22.62-9.375L160 301.3L54.63 406.6C48.38 412.9 40.19 416 32 416S15.63 412.9 9.375 406.6c-12.5-12.5-12.5-32.75 0-45.25l105.4-105.4L9.375 150.6c-12.5-12.5-12.5-32.75 0-45.25s32.75-12.5 45.25 0L160 210.8l105.4-105.4c12.5-12.5 32.75-12.5 45.25 0s12.5 32.75 0 45.25l-105.4 105.4L310.6 361.4z"/></svg>
+
+ </span>
+
+</span>
+ </li>
+
+
+
+
+ <li class="mt-1">
+ <a href="" class="flex items-center text-gray-500 hover:text-primary-600 dark:hover:text-primary-400">
+
+ <p class="text-bg font-bg" title="">
+ about
+ </p>
+ </a>
+</li>
+
+
+
+
+
+
+ <li class="mt-1">
+ <a href="/posts/" class="flex items-center text-gray-500 hover:text-primary-600 dark:hover:text-primary-400">
+
+ <p class="text-bg font-bg" title="">
+ blog
+ </p>
+ </a>
+</li>
+
+
+
+
+
+
+ <li class="mt-1">
+ <a href="/tags/" class="flex items-center text-gray-500 hover:text-primary-600 dark:hover:text-primary-400">
+
+ <p class="text-bg font-bg" title="">
+ tags
+ </p>
+ </a>
+</li>
+
+
+
+
+
+ </ul>
+
+
+
+ </div>
+ </label>
+ </div>
+</div>
+
+
+
+
+<script>
+ (function () {
+ var $mainmenu = $('.main-menu');
+ var path = window.location.pathname;
+ $mainmenu.find('a[href="' + path + '"]').each(function (i, e) {
+ $(e).children('p').addClass('active');
+ });
+ })();
+</script>
+
+
+
+ <div class="relative flex flex-col grow">
+ <main id="main-content" class="grow">
+
+
+
+<article>
+
+
+ <header id="single_header" class="mt-5 max-w-prose">
+
+ <ol class="text-sm text-neutral-500 dark:text-neutral-400 print:hidden">
+
+
+
+
+
+
+ <li class="inline hidden">
+ <a
+ class="hover:underline decoration-neutral-300 dark:underline-neutral-600"
+ href="/"
+ >lowest case</a
+ ><span class="px-1 text-primary-500">/</span>
+ </li>
+
+
+ <li class="inline ">
+ <a
+ class="hover:underline decoration-neutral-300 dark:underline-neutral-600"
+ href="/posts/"
+ >posts</a
+ ><span class="px-1 text-primary-500">/</span>
+ </li>
+
+
+ <li class="inline hidden">
+ <a
+ class="hover:underline decoration-neutral-300 dark:underline-neutral-600"
+ href="/posts/correctness-is-all-you-need/"
+ >correctness is all you need</a
+ ><span class="px-1 text-primary-500">/</span>
+ </li>
+
+</ol>
+
+
+
+ <h1 class="mt-0 text-4xl font-extrabold text-neutral-900 dark:text-neutral">
+ correctness is all you need
+ </h1>
+ <div class="mt-1 mb-6 text-base text-neutral-500 dark:text-neutral-400 print:hidden">
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+<div class="flex flex-row flex-wrap items-center">
+
+
+ <time datetime="2024-05-09 23:35:32 -0300 -03">9 May 2024</time><span class="px-2 text-primary-500">&middot;</span><span title="reading time">1 min</span>
+
+
+
+
+</div>
+
+
+
+
+
+<div class="flex flex-row flex-wrap items-center">
+
+
+
+
+
+
+
+
+
+
+
+
+ <span style="margin-top:0.5rem" class="mr-2" onclick="window.open(&#34;/tags/coq/&#34;,'_self');">
+ <span class="flex" style="cursor: pointer;">
+ <span class="rounded-md border border-primary-400 px-1 py-[1px] text-xs font-normal text-primary-700 dark:border-primary-600 dark:text-primary-400">
+ coq
+ </span>
+</span>
+ </span>
+
+ <span style="margin-top:0.5rem" class="mr-2" onclick="window.open(&#34;/tags/rust/&#34;,'_self');">
+ <span class="flex" style="cursor: pointer;">
+ <span class="rounded-md border border-primary-400 px-1 py-[1px] text-xs font-normal text-primary-700 dark:border-primary-600 dark:text-primary-400">
+ rust
+ </span>
+</span>
+ </span>
+
+
+
+
+</div>
+
+
+
+ </div>
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ </header>
+
+ <section class="flex flex-col max-w-full mt-0 prose dark:prose-invert lg:flex-row">
+
+
+
+ <div class="min-w-0 min-h-0 max-w-fit">
+
+
+
+
+ <div class="article-content max-w-prose mb-20">
+ <div class="highlight"><pre tabindex="0" class="chroma"><code class="language-python" data-lang="python"><span class="line"><span class="cl"><span class="o">&gt;&gt;&gt;</span> <span class="mf">0.1</span> <span class="o">+</span> <span class="mf">0.2</span>
+</span></span><span class="line"><span class="cl"><span class="mf">0.30000000000000004</span>
+</span></span></code></pre></div><p>which of course is an annoying encounter for the unitiated in floats, but there&rsquo;s a much bigger problem, that usually isn&rsquo;t noticed at all until much later, that float addition itself isn&rsquo;t even associative:</p>
+<div class="highlight"><pre tabindex="0" class="chroma"><code class="language-python" data-lang="python"><span class="line"><span class="cl"><span class="o">&gt;&gt;&gt;</span> <span class="p">(</span><span class="mf">0.1</span> <span class="o">+</span> <span class="mf">0.2</span><span class="p">)</span> <span class="o">+</span> <span class="mf">0.3</span>
+</span></span><span class="line"><span class="cl"><span class="mf">0.6000000000000001</span>
+</span></span><span class="line"><span class="cl"><span class="o">&gt;&gt;&gt;</span> <span class="mf">0.1</span> <span class="o">+</span> <span class="p">(</span><span class="mf">0.2</span> <span class="o">+</span> <span class="mf">0.3</span><span class="p">)</span>
+</span></span><span class="line"><span class="cl"><span class="mf">0.6</span>
+</span></span><span class="line"><span class="cl"><span class="o">&gt;&gt;&gt;</span> <span class="mf">0.1</span> <span class="o">+</span> <span class="p">(</span><span class="mf">0.2</span> <span class="o">+</span> <span class="mf">0.3</span><span class="p">)</span> <span class="o">==</span> <span class="p">(</span><span class="mf">0.1</span> <span class="o">+</span> <span class="mf">0.2</span><span class="p">)</span> <span class="o">+</span> <span class="mf">0.3</span>
+</span></span><span class="line"><span class="cl"><span class="kc">False</span>
+</span></span><span class="line"><span class="cl"><span class="o">&gt;&gt;&gt;</span>
+</span></span></code></pre></div><p>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:</p>
+<ul>
+<li>not all numbers have an additive inverse, ie. for some number <code>n</code>, <code>n + (-n) != n</code>.</li>
+<li>not all numbers different than 0 have a multiplicative inverse, ie. for some number <code>n</code>, <code>n / n != 1</code>.</li>
+<li>addition is not commutative, ie. for numbers <code>a</code> <code>b</code>, <code>a + b != b + a</code>.</li>
+</ul>
+<p>and the list goes you on, you get the idea. this usually isn&rsquo;t thought of the main problems in</p>
+
+ </div>
+
+
+
+
+
+
+
+ </div>
+
+
+
+
+
+
+
+
+ <script>
+ var oid = "views_posts\/correctness-is-all-you-need.md"
+ var oid_likes = "likes_posts\/correctness-is-all-you-need.md"
+ </script>
+
+
+
+ <script type="text/javascript" src="/js/page.min.b06a29d42a4ed16787978e2eee1e8c797b7698db2bc14ccee78f5c80ac566fc996190a73ad80a5e987558474b20b96fa38f7d85b405f165ff72b7b163c5ad11b.js" integrity="sha512-sGop1CpO0WeHl44u7h6MeXt2mNsrwUzO549cgKxWb8mWGQpzrYCl6YdVhHSyC5b6OPfYW0BfFl/3K3sWPFrRGw=="></script>
+
+ </section>
+ <footer class="pt-8 max-w-prose print:hidden">
+
+
+
+
+
+
+ </footer>
+</article>
+
+ <div id="top-scroller" class="pointer-events-none absolute top-[110vh] bottom-0 w-12 ltr:right-0 rtl:left-0">
+ <a href="#the-top"
+ class="pointer-events-auto sticky top-[calc(100vh-5.5rem)] flex h-12 w-12 mb-16 items-center justify-center rounded-full bg-neutral/50 text-xl text-neutral-700 hover:text-primary-600 dark:bg-neutral-800/50 dark:text-neutral dark:hover:text-primary-400"
+ aria-label="scroll to top" title="scroll to top">
+ &uarr;
+ </a>
+</div>
+ </main><footer id="site-footer" class="py-10 print:hidden">
+
+
+
+
+ <div class="flex items-center justify-between">
+
+
+
+ <p class="text-sm text-neutral-500 dark:text-neutral-400">
+ &copy;
+ 2024
+ leonardo santiago
+ </p>
+
+
+
+
+ <p class="text-xs text-neutral-500 dark:text-neutral-400">
+
+
+ powered by <a class="hover:underline hover:decoration-primary-400 hover:text-primary-500"
+ href="https://gohugo.io/" target="_blank" rel="noopener noreferrer">Hugo</a> &amp; <a class="hover:underline hover:decoration-primary-400 hover:text-primary-500"
+ href="https://blowfish.page/" target="_blank" rel="noopener noreferrer">Blowfish</a>
+ </p>
+
+
+ </div>
+ <script>
+
+ mediumZoom(document.querySelectorAll("img:not(.nozoom)"), {
+ margin: 24,
+ background: 'rgba(0,0,0,0.5)',
+ scrollOffset: 0,
+ })
+
+ </script>
+
+
+ <script type="text/javascript" src="/js/process.min.62060bb247f4de2b6dde45903668fefb68d792f365587605177b1227c0cf43588701edaca0cb40e2c8e2789bd5ce67c1d2a215b9fb258c3496a7cd25e7cb5fdf.js" integrity="sha512-YgYLskf03itt3kWQNmj&#43;&#43;2jXkvNlWHYFF3sSJ8DPQ1iHAe2soMtA4sjieJvVzmfB0qIVufsljDSWp80l58tf3w=="></script>
+
+
+</footer><div
+ id="search-wrapper"
+ class="invisible fixed inset-0 flex h-screen w-screen cursor-default flex-col bg-neutral-500/50 p-4 backdrop-blur-sm dark:bg-neutral-900/50 sm:p-6 md:p-[10vh] lg:p-[12vh]"
+ data-url="http://localhost:1313/"
+ style="z-index:500"
+>
+ <div
+ id="search-modal"
+ class="flex flex-col w-full max-w-3xl min-h-0 mx-auto border rounded-md shadow-lg top-20 border-neutral-200 bg-neutral dark:border-neutral-700 dark:bg-neutral-800"
+ >
+ <header class="relative z-10 flex items-center justify-between flex-none px-2">
+ <form class="flex items-center flex-auto min-w-0">
+ <div class="flex items-center justify-center w-8 h-8 text-neutral-400">
+
+
+ <span class="relative block icon">
+ <svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="search" class="svg-inline--fa fa-search fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M505 442.7L405.3 343c-4.5-4.5-10.6-7-17-7H372c27.6-35.3 44-79.7 44-128C416 93.1 322.9 0 208 0S0 93.1 0 208s93.1 208 208 208c48.3 0 92.7-16.4 128-44v16.3c0 6.4 2.5 12.5 7 17l99.7 99.7c9.4 9.4 24.6 9.4 33.9 0l28.3-28.3c9.4-9.4 9.4-24.6.1-34zM208 336c-70.7 0-128-57.2-128-128 0-70.7 57.2-128 128-128 70.7 0 128 57.2 128 128 0 70.7-57.2 128-128 128z"/></svg>
+
+ </span>
+
+
+ </div>
+ <input
+ type="search"
+ id="search-query"
+ class="flex flex-auto h-12 mx-1 bg-transparent appearance-none focus:outline-dotted focus:outline-2 focus:outline-transparent"
+ placeholder="cearch"
+ tabindex="0"
+ />
+ </form>
+ <button
+ id="close-search-button"
+ class="flex items-center justify-center w-8 h-8 text-neutral-700 hover:text-primary-600 dark:text-neutral dark:hover:text-primary-400"
+ title="close (Esc)"
+ >
+
+
+ <span class="relative block icon">
+ <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 320 512"><path fill="currentColor" d="M310.6 361.4c12.5 12.5 12.5 32.75 0 45.25C304.4 412.9 296.2 416 288 416s-16.38-3.125-22.62-9.375L160 301.3L54.63 406.6C48.38 412.9 40.19 416 32 416S15.63 412.9 9.375 406.6c-12.5-12.5-12.5-32.75 0-45.25l105.4-105.4L9.375 150.6c-12.5-12.5-12.5-32.75 0-45.25s32.75-12.5 45.25 0L160 210.8l105.4-105.4c12.5-12.5 32.75-12.5 45.25 0s12.5 32.75 0 45.25l-105.4 105.4L310.6 361.4z"/></svg>
+
+ </span>
+
+
+ </button>
+ </header>
+ <section class="flex-auto px-2 overflow-auto">
+ <ul id="search-results">
+
+ </ul>
+ </section>
+ </div>
+</div>
+
+ </div>
+</body>
+
+</html>
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-23 09:32:52 +0000