Jesse Alama @ Igaliaurn:uuid:7bcad992-a5b8-4bb0-ba30-54af443615942024-04-04T02:07:27ZJesse Alamajesse@igalia.comPollenHere’s how to unbreak floating-point math in JavaScripturn:uuid:9f3e05be-4e83-4b8c-905d-d68d4b872459Just discover that 0.1 + 0.2 isn’t 0.3 in JavaScript? WTF? What’s wrong? Can anything be done? Yes! (Though it may take some time.)<main><h1 id="unbreaking-floating-point-math-in-javascript">Unbreaking floating-point math in JavaScript</h1><p>Because computers are limited, they work in a finite range of numbers, namely, those that can be represented straightforwardly as fixed-length (usually 32 or 64) sequences of bits. If you’ve only got 32 or 64 bits, it’s clear that there are only so many numbers you can represent, whether we’re talking about integers or decimals. For integers, it’s clear that there’s a way to exactly represent mathematical integers (within the finite domain permitted by 32 or 64 bits). For decimals, we have to deal with the limits imposed by having only a fixed number of bits: most decimal numbers cannot be exactly represented. This leads to headaches in all sorts of contexts where decimals arise, such as finance, science, engineering, and machine learning.</p><p>It has to do with our use of base 10 and the computer’s use of base 2. <small>Math strikes again!</small> Exactness of decimal numbers isn’t an abstruse, edge case-y problem that some mathematicians thought up to poke fun at programmers engineers who aren’t blessed to work in an infinite domain. Consider a simple example. Fire up your favorite JavaScript engine and evaluate this:</p><pre class="brush: javascript"><code>1 + 2 === 3</code></pre><p>You should get <code>true</code>. Duh. But take that example and work it with decimals:</p><pre class="brush: javascript"><code>0.1 + 0.2 === 0.3</code></pre><p>You’ll get <code>false</code>.</p><p>How can that be? Is floating-point math broken in JavaScript? Short answer: yes, it is. But if it’s any consolation, it’s not <em>just</em> JavaScript that’s broken in this regard. You’ll get the same result in all sorts of other languages. This isn’t <a href="https://www.destroyallsoftware.com/talks/wat">wat</a>. This is the unavoidable burden we programmers bear when dealing with decimal numbers on machines with limited precision.</p><p>Maybe you’re thinking <q>OK, but if that’s right, how in the world do decimal numbers get handled at all? Think of all the financial applications out there that must be doing the wrong thing countless times a day.</q> You’re quite right! One way of getting around oddities like the one above is by always rounding. So instead of working with, say, this is by handling decimal numbers as strings (sequences of digits). You would then define operations such as addition, multiplication, and equality by doing elementary school math, digit by digit (or, rather, character by character).</p><h2 id="so-what-to-do">So what to do?</h2><p>Numbers in JavaScript are <a href="https://262.ecma-international.org/12.0/#sec-mathematical-operations">supposed</a> to be IEEE 754 floating-point numbers. A consequence of this is, effectively, that <code>0.1 + 0.2</code> will <em>never</em> be <code>0.3</code> (in the sense of the <code>===</code> operator in JavaScript). So what can be done?</p><p>There’s an npm library out there, <a href="https://www.npmjs.com/package/decimal.js">decimal.js</a>, that provides support for arbitrary precision decimals. There are probably other libraries out there that have similar or equivalent functionality.</p><p>As you might imagine, the issue under discussion is old. There are workarounds using a library.</p><p>But what about extending the language of JavaScript so that the equation <em>does</em> get validated? Can we make JavaScript work with decimals correctly, without using a library?</p><p>Yes, we can.</p><h2 id="aside-huge-integers">Aside: Huge integers</h2><p>It’s worth thinking about a similar issue that also arises from the finiteness of our machines: arbitrarily large integers in JavaScript. Out of the box, JavaScript didn’t support extremely large integers. You’ve got 32-bit or (more likely) 64-bit signed integers. But even though that’s a big range, it’s still, of course, limited. <a href="https://www.proposals.es/proposals/BigInt">BigInt</a>, a proposal to extend JS with precisely this kind of thing, <a href="https://github.com/tc39/proposal-bigint/commit/771df8ff3516ea5f3397153d17d04e6c6b75a4ce">reached Stage 4 in 2019</a>, so it should be available in <a href="https://caniuse.com/?search=bigint">pretty much every JavaScript engine you can find</a>. Go ahead and fire up Node or open your browser’s inspector and plug in the number of nanoseconds since the Big Bang:</p><pre class="brush: javascript"><code>13_787_000_000_000n // years * 365n // days * 24n // hours * 60n // minutes * 60n // seconds * 1000n // milliseconds * 1000n // microseconds * 1000n // nanoseconds</code></pre><p><small>(Not a scientician. May not be true. Not intended to be a factual claim.)</small></p><h2 id="adding-big-decimals-to-the-language">Adding big decimals to the language</h2><p>OK, enough about big integers. What about adding support for arbitrary precision decimals in JavaScript? Or, at least, high-precision decimals? As we see above, we don’t even need to wrack our brains trying to think of complicated scenarios where a ton of digits after the decimal point are needed. Just look at 0.1 + 0.2 = 0.3. That’s pretty low-precision, and it still doesn’t work. Is there anything analogous to BigInt for non-integer decimal numbers? No, not as a library; we already discussed that. Can we add it to the language, so that, out of the box—with no third-party library—we can work with decimals?</p><p>The answer is <q>yes</q>. Work is proceeding on this matter, but things remain to unsettled. The relevant proposal is <a href="https://github.com/tc39/proposal-decimal">BigDecimal</a>. I’ll be working on this for a while. I want to get big decimals into JavaScript. There are all sorts of issues to resolve, but they’re definitely resolvable. We have experience with arbitrary precision arithmetic in other languages. It can be done.</p><p>So yes, <a href="https://stackoverflow.com/questions/588004/is-floating-point-math-broken?rq=1">floating-point math is broken</a> in JavaScript, but help is on the way. You’ll see more from me here as I tackle this interesting problem; stay tuned!</p></main>2022-11-14T11:33:24ZQuickJS already supports arbitrary-precision decimalsurn:uuid:9f331363-1dac-467f-82d4-34143d6ef7a8QuickJS is a JavaScript engine that supports arbitrary-precision decimals. Here’s how to play around with them.<main><h1>QuickJS already supports arbitrary-precision decimals</h1><p><a href="https://bellard.org/quickjs/" title="QuickJS">QuickJS</a> is a neat JavaScript engine by <span itemscope="" itemtype="https://schema.org/Person" class="person"><a itemprop="url" href="https://bellard.org" title="Fabrice Bellard"><span itemprop="givenName">Fabrice</span> <span itemprop="familyName">Bellard</span></a></span>. It’s fast and small (version 2021-03-27 clocks in at 759 Kb). It includes support for arbitrary-precision decimals, even though <a href="https://www.proposals.es/proposals/Decimal" title="Decimal (proposals.es)">the TC39 decimal proposal</a> is (at the time of writing) still at Stage 2. You can install it using the tool of your choice; I was able to install it using Homebrew for macOS (the formula is called <code>quickjs</code>) and FreeBSD and OpenBSD. It can also be installed using <a href="https://github.com/devsnek/esvu" title="esvu: Your one-stop shop for all implementations of ECMAScript">esvu</a>. (It doesn’t seem to be available as a package on Ubuntu.)</p><p>To get started with arbitrary precision decimals, you need to fire up QuickJS with the <code>bignum</code> flag:</p><pre>$ qjs --bignum<br/>QuickJS - Type "\h" for help<br/>qjs > 0.1 + 0.2 === 0.3<br/>false<br/>qjs > 0.1m + 0.2m === 0.3m<br/>true<br/>qjs > 0.12345678910111213141516171819m * 0.19181716151413121110987654321m<br/>0.0236811308550240594910066199325923006903586430678413779899m</pre><p>(The <code>m</code> is the proposed suffix for literal high-precision decimal numbers that proposal-decimal is supposed to give us.) Notice how we nicely <a href="/unbreaking-floating-point-math-in-js/" title="Here’s how to unbreak floating-point math in JavaScript">unbreak</a> JavaScript decimal arithmetic, without having to load a library.</p><p>The final API in the official TC39 Decimal proposal still has not been worked out. Indeed, a core question there remains outstanding at the time of writing: what kind of numeric precision should be supported? (The two main contenders are arbitrary precision and the other being 128-bit IEEE 754 (high, but not *arbitrary*, precision). QuickJS does arbitrary precision.) Nonetheless, QuickJS provides a <code>BigDecimal</code> function:</p><pre>qjs > BigDecimal("123456789.0123456789")<br/>123456789.0123456789m</pre><p>Moreover, you can do basic arithmetic with decimals: addition, subtraction, multiplication, division, modulo, square roots, and rounding. Everything is done with infinite precision (no loss of information). If you know, in advance, what precision is needed, you can tweak the arithmetical operations by passing in an options argument. Here’s an example of adding two big decimal numbers:</p><pre>qjs > var a = 0.12345678910111213141516171819m;<br/>undefined<br/>qjs > var b = 0.19181716151413121110987654321m;<br/>undefined<br/>qjs > BigDecimal.add(a,b)<br/>0.3152739506152433425250382614m<br/>qjs > BigDecimal.add(a,b, { "roundingMode": "up", "maximumFractionDigits": 10 })<br/>0.3152739507m</pre></main>2022-11-15T08:42:15ZA comprehensive, authoritative FAQ on decimal arithmeticurn:uuid:5cadc0a2-7de1-4f23-b871-90c01def8dfeMike Cowlishaw, editor of the 2008 edition of the IEEE 754 floating-point arithmetic standard, has a delightful FAQ page on decimal arithmetic.<main><h1>Mike Cowlishaw’s FAQ on decimal arithmetic</h1><p>If you’re interested in decimal arithmetic in computers, you’ve got to check out <a href="https://speleotrove.com/decimal/decifaq1.html" title="Decimal Arithmetic FAQ ">Mike Cowlishaw’s FAQ</a> on the subject. There’s a ton of insight to be had there. If you like the kind of writing that makes you feel smarter as you read it, this one is worth your time.</p><p>For context: Cowlishaw is the editor of the 2008 edition of the <a href="https://ieeexplore.ieee.org/document/4610935" title="754-2008 - IEEE Standard for Floating-Point Arithmetic (IEEE Xplore)">IEEE 754 standard</a>, updating the 1985 and 1987 standards. The words thus carry a lot of authority, and it would be quite unwise to ignore Mike in these matters.</p><p>If you prefer similar information in article form, take a look at Mike’s <span class="paper"><a href="https://speleotrove.com/decimal/IEEE-cowlishaw-arith16.pdf" title="Decimal Floating-Point: Algorism for Computers ">Decimal Floating-Point: Algorism for Computers</a></span>. (Note the delightful use of <q>algorism</q>. Yes, it’s a <a href="https://en.wikipedia.org/wiki/Algorism" title="Algorism (Wikipedia)">word</a>.)</p><p>The FAQ focused mainly on <em>floating-point</em> decimal arithmetic, not arbitrary-precision decimal arithmetic (which is what one might immediately think of when the one hears <q>decimal arithmetic</q>). Arbitrary-precision decimal arithmetic is whole other ball of wax. In that setting, we’re talking about sequences of decimal digits whose length cannot be specified in advance. Proposals such as <a href="https://en.wikipedia.org/wiki/Decimal128_floating-point_format" title="decimal128 floating-point format (Wikipedia)">decimal128</a> are about a fixed bit width—128 bits—which allows for a <em>lot</em> of precision, but not <em>arbitrary</em> precision.</p><p>One crucial insight I take away from Mike’s FAQ—a real misunderstanding on my part which is a bit embarrassing to admit—is that decimal128 is not just a 128-bit version of the same old binary floating-point arithmetic we all know about (and might find <a href="/unbreaking-floating-point-math-in-js/">broken</a>). It’s not as though adding more bits meets the demands of those who want high-precision arithmetic. No! Although decimal128 is a fixed-width encoding (128 bits), the underlying encoding is <em>decimal</em>, not binary. That is, decimal128 isn’t just binary floating-point with extra juice. Just adding bits won’t unbreak busted floating-point arithmetic; some new ideas are needed. And decimal128 is a way forward. It is a new (well, relatively new) format that addresses all sorts of use cases that motivate decimal arithmetic, including needs in business, finance, accounting, and anything that uses <q>human</q> decimal numbers. What probably led to my confusion is thinking that the adjective <q>floating-point</q>, regardless of what it modifies, must be some kind of variation of binary floating-point arithmetic.</p></main>2022-12-13T08:36:46ZBinary floats can let us down! When close enough isn't enoughurn:uuid:9ebb438d-078e-4cdd-8fdc-85155678057bStandard IEEE-754 binary floating point numbers can let us down, even on simple calcualtions. Or: is your bill correct?<main><h1>How binary floating points can let us down</h1><p>If you've played <em>Monopoly</em>, you'll know abuot the <q>Bank Error in Your Favor</q> card in the Community Chest. Remember this?</p><p><img src="community-chest-bank-error-in-your-favor.jpg" title="Card from the game Monopoly: Bank error in your favor!"/></p><p>A bank error in your favor? Sweet! But what if the bank makes an error in <em>its</em> favor? Surely that's just as possible, right?</p><p>I'm here to tell you that if you're doing everyday financial calculations—nothing fancy, but involving money that you care about—then you might need to know that using binary floating point numbers, then something might be going wrong. Let's see how binary floating-point numbers might yield bank errors in your favor—or the bank's.</p><p>In a wonderful paper on decimal floating-point numbers, Mike Colishaw gives an example.</p><p>Here's how you can reproduce that in JavaScript:</p><div class="highlight"><pre><code>(1.05 * 0.7).toPrecision(2); # 0.73</code></pre></div><p>Some programmers might not be aware of this, but many are. By pointing this out I'm not trying to be a smartypants who knows something you don't. For me, this example illustrates just how common this sort of error might be.</p><p>For programmers who are aware of the issue, one typical approache to dealing with it is this: <em>Never work with sub-units of a currency.</em> (Some currencies don't have this issue. If that's you and your problem domain, you can kick back and be glad that you don't need to engage in the following sorts of headaches.) For instance, when working with US dollars of euros, this approach mandates that one never works with euros and cents, but only with cents. In this setting, dollars exist only as an abstraction on top of cents. As far as possible, calculations never use floats. But if a floating-point number threatens to come up, some form of rounding is used.</p><p>Another aproach for a programmer is to delegate financial calculations to an external system, such as a relational database, that natively supports proper decimal calculations. One difficulty is that even if one delegates these calculations to an external system, if one lets a floating-point value flow int your program, even a value that can be trusted, it may become tainted just by being imported into a language that doesn't properly support decimals. If, for instance, the result of a calculation done in, say, Postgres, is exactly 0.1, and that flows into your JavaScript program as a number, it's possible that you'll be dealing with a contaminated value. For instance:</p><div class="highlight"><pre><code>(0.1).toPrecision(25) # 0.1000000000000000055511151</code></pre></div><p>This example, admittedly, requires quite a lot of decimals (19!) before the ugly reality of the situation rears its head. The reality is that 0.1 does not, and cannot, have an exact representation in binary. The earlier example with the cost of a phone call is there to raise your awareness of the possibility that one doesn't need to go 19 decimal places before one starts to see some weirdness showing up.</p><p>There are all sorts of examples of this. It's exceedingly rare for a decimal number to have an exact representation in binary. Of the numbers 0.1, 0.2, …, 0.9, only 0.5 can be exactly represented in binary.</p><p>Next time you look at a bank statement, or a bill where some tax is calculated, I invite you to ask how that was calculated. Are they using decimals, or floats? Is it correct?</p><p>I'm working on the decimal proposal for TC39 to try to work what it might be like to add proper decimal numbers to JavaScript. There are a few very interesting degrees of freedom in the design space (such as the precise datatype to be used to represent these kinds of number), but I'm optimistic that a reasonable path forward exists, that consensus between JS programmers and JS engine implementors can be found, and eventually implemented. If you're interested in these issues, check out the README in the proposal and get in touch!</p></main>2023-09-19T08:37:44ZAnnouncing decimal128: JavaScript implementation of Decimal128urn:uuid:3da4cbb4-c342-4b74-9858-75e3dcf67f5aI've made an NPM package that allows you to work with IEEE 754 Decimal128 values in your JavaScript programs. Time to start working with decimal numbers!<main><h1 id="announcing-decimal128js-an-npm-package-for-ieee-754-decimal128-floating-point-decimal-numbers">Announcing <code>decimal128.js</code>, an NPM package for IEEE 754 Decimal128 floating-point decimal numbers</h1><p>I’m happy to announce <a href="https://www.npmjs.com/package/decimal128"><code>decimal128.js</code></a>, an NPM package I made for simulating <a href="https://en.wikipedia.org/wiki/Decimal128_floating-point_format">IEEE 754 Decimal128</a> numbers in JavaScript.</p><p>(This is my first NPM package. I made it in TypeScript; it’s my first go at the language.)</p><h2 id="what">What?</h2><p>Decimal128 is an IEEE standard for floating-point decimal numbers. These numbers aren’t the binary floating-point numbers that you know and love (?), but <em>decimal</em> numbers. You know, the kind we learn about before we’re even ten years old. In the binary world, things like <code>0.1 + 0.2</code> aren’t <em>exactly</em>* equal to <code>0.3</code>, and calculations like <code>0.7 * 1.05</code> work out to <em>exactly</em> <code>0.735</code>. These kinds of numbers are what we use when doing all sorts of everyday calculations, especially those having to do with money.</p><p>Decimal128 encodes decimal numbers into 128 bits. It is a fixed-width encoding, unlike arbitrary-precision numbers, which, of course, require an arbitrary amount of space. The encoding can represent of numbers with up to 34 significant digits and an exponent of –6143 to 6144. That is a truly vast amount of space if one keeps the intended use cases involving human-readable and -writable numbers (read: money) in mind.</p><h2 id="why">Why?</h2><p>I’m working on extending the JavaScript language with decimal numbers (<a href="https://github.com/tc39/proposal-decimal">proposal-decimal</a>). One of the design decisions that has to be made there is whether to implement arbitrary-precision decimal numbers or to implement some kind of approximation thereof, with Decimal128 being the main contender. As far as I could tell, there was no implementation of Decimal128 in JavaScript, so I made one.</p><p>The intention isn’t to support the full Decimal128 standard, nor should one expect to achieve the performance that, say, a C/C++ library would give you in userland JavaScript. (To say nothing of having <em>machine-native</em> decimal instructions, which is truly exotic.) The intention is to give JavaScript developers something that genuinely strives to approximate Decimal128 for JS programs.</p><p>In particular, the hope is that this library offers the JS community a chance to get a feel for what Decimal128 might be like.</p><h2 id="how-to-use">How to use</h2><p>Just do</p><pre class="brush: sh"><code>$ npm install decimal128</code></pre><p>and start using the provided <code>Decimal128</code> class.</p><h2 id="issues">Issues?</h2><p>If you find any bugs or would like to request a feature, just open an <a href="https://github.com/jessealama/decimal128.js/issues">issue</a> and I’ll get on it.</p></main>2023-05-09T11:26:38ZNative support for decimal numbers in the Python programming languageurn:uuid:4962cf6e-d794-4344-a1ed-a726b346d8a5The Python programming langauge supports decimal numbers in its standard library. Here’s a summary of how to work with this important data type.<main><h1>Native support for decimal numbers in the Python programming language</h1><p>As part of the project of exploring how decimal numbers could be added to JavaScript, I'd like to take a step back and look at how other languages support decimals (or not). Many languages do support decimal numbers. It may be useful to understand the range of options out there for supporting them. For instance, what kind of data model do they use? What are the limits (if there are any)? Does the langauge include any special syntax for decimal?</p><p>Here, I'd like to briefly summarize what <b>Python</b> has done.</p><h2>Does Python support decimals?</h2><p>Python <a href="https://docs.python.org/3/library/decimal.html">supports decimal arithmetic</a>. The functionality is part of the standard library. Decimals aren't available out-of-the-box, in the sense that all Python programs, regardless of what they import, can start working with decimals. There is no decimal literal syntax in the language. That said, all one needs to do is <code>import * from decimal</code> and you're ready to rock.</p><p>Decimals have been part of the Python standard library for a <em>long</em> time: they were added in <a href="https://docs.python.org/2.4/whatsnew/">version 2.4</a>, in November 2001. Python does have a process for proposing extensions to the language, called PEP (Python Extension Proposal). Extensive discussions on the official mailing lists took place. Python decimals were formalized in <a href="https://peps.python.org/pep-0327/">PEP 327</a>.</p><p>The decimal library provides access to some of the internals of decimal arithmetic, called the <em>context</em>. In the context, one can specify, for instance, the number of decimal digits that should be available when operations are carried out. One can also forbid mixing of decimal values with primitive built-in types, such as integers and (binary) floating-point numbers.</p><p>In general, the Python implementation aims to be an implementation of the <a href="https://speleotrove.com/decimal/decarith.html">General Decimal Arithmetic Specification</a>. In particular, using this data model, it is possible to distinguish the digit strings <code>1.2</code> and <code>1.20</code>, considered as decimal values, as mathematically equal but nonetheless distinct values.</p><p>Aside: <em>How does this compare with Decimal128</em>, one of the contender data models for decimals in JavaScript? Since Python's decimal feature is an implementation of the General Decimal Arithmetic Specification, it works with a sort of generalized IEEE 754 Decimal. No bit width is specified, so Python decimals are not literally the same as Decimal128. However, one can suitably parameterize Python's decimal to get something essentially equivalent to Decimal128:</p><ol><li>specify the minimum and maximum exponent to -6144 and 6143, respectively (the defaults are -999999 and 999999, respectively)</li><li>specify the precision to 34 (default is 28)</li></ol><h2>API for Python decimals</h2><p>Here are the supported mathematical functions:</p><ul><li>basic arithmetic: addition, subtraction, subtraction, division</li><li>natural exponentiation and log (<em>e^x</em>, ln(<em>x</em>))</li><li>log base 10</li><li><em>a^b</em> (two-argument exponentiation, though the exponent needs to be an integer)</li><li>step up/down (1.451 → 1.450, 1.452)</li><li>square root</li><li>fused multiply-and-add (<em>a*b + c</em>)</li></ul><p>As mentioned above, the data model for Python decimals allows for subnormal decimals, but one can always normalize a value (remove the trailing zeros). (This isn't exactly a mathematical function, since distinct members of a cohort are mathematically equal.)</p><p>In Python, when importing decimals, some of the basic arithmetic operators get overloaded. Thus, <code>+</code>, <code>*</code>, and <code>**</code>, etc., produce correct decimal results when given decimal arguments. (There is <a href="https://github.com/tc39/proposal-operator-overloading">some possibility</a> for something roughly similar in JavaScript, but that discussion has been paused.)</p><p>Trigonometric functions are not provided. (These functions belong to the <q>optional</q> part of the IEEE 754 specification.)</p></main>2023-10-30T03:14:15ZThe decimals around us: Cataloging support for decimal numbersurn:uuid:3835a42d-5548-48d9-aa63-e23df3829609Many programming languages have support for decimals in various forms. Here is a catalog of where they stand regarding their support for decimals.<main><h1>A catalog of support for decimal numbers in various programming languages</h1><p>Decimals numbers are a data type that aims to exactly represent decimal numbers. Some programmers may not know, or fully realize, that, in most programming languages, the numbers that you enter <em>look</em> like decimal numbers but internally are represented as binary—that is, base-2—floating-point numbers. Things that are totally simple for us, such as <code>0.1</code>, simply cannot be represented exactly in binary. The decimal data type—whatever its stripe or flavor—aims to remedy this by giving us a way of representing and working with decimal numbers, not binary approximations thereof. (Wikipedia has <a href="https://en.wikipedia.org/wiki/Decimal_data_type">more</a>.)</p><p>To help with my work on adding decimals to JavaScript, I've gone through a list of popular programming languages, taken from <a href="https://survey.stackoverflow.co/2022/#technology-most-popular-technologies">the 2022 StackOverflow developer survey</a>. What follows is a brief summary of where these languages stand regarding decimals. The intention is to keep things simple. The purpose is:</p><ol><li>If a language does have decimals, say so;</li><li>If a language does not have decimals, but at least one third-party library exists, mention it and link to it. If a discussion is underway to add decimals to the language, link to that discussion.</li></ol><p>There is no intention to filter out an language in particular; I'm just working with a slice of languages found in in the StackOverflow list linked to earlier. If a language does not have decimals, there may well be multiple third-part decimal libraries. I'm not aware of all libraries, so if I have linked to a <q>minor</q> library and neglect to link to a more high-profile one, please let me know. More importantly, if I have misrepresented the basic fact of whether decimals exists at all in a language, <a href="mailto:hi@jessealama.net">send mail</a>.</p><section><h2>C</h2><p>C does <strong>not</strong> have decimals. But they're working on it! The <a href="https://en.wikipedia.org/wiki/C23_(C_standard_revision)">C23 standard</a> (as in, 2023) standard proposes to add new fixed bit-width data types (32, 64, and 128) for these numbers.</p></section><section><h2>C#</h2><p>C# <a href="https://learn.microsoft.com/en-us/dotnet/api/system.decimal?view=net-7.0">has</a> decimals in its underlying .NET subsystem. (For the same reason, decimals also exist in Visual Basic.)</p></section><section><h2>C++</h2><p>C++ does <strong>not</strong> have decimals. But—like C—they're <a href="https://isocpp.org/files/papers/P2159R1.html">working</a> on it!</p></section><section><h2>Dart</h2><p>Dart does <strong>not</strong> have decimals. But a third-party library <a href="https://pub.dev/documentation/decimal/latest/">exists</a>.</p></section><section><h2>Go</h2><p>Go does not have decimals, but a third-party library <a href="https://pkg.go.dev/github.com/shopspring/decimal#section-readme">exists</a>.</p></section><section><h2>Java</h2><p>Java <a href="https://docs.oracle.com/javase/8/docs/api/java/math/BigDecimal.html">has</a> decimals.</p></section><section><h2>JavaScript</h2><p>JavaScript does not have decimals. We're <a href="https://github.com/tc39/proposal-decimal/">working</a> on it!</p></section><section><h2>Kotlin</h2><p>Kotlin does not have decimals. But, in a way, it does: since Kotlin is running on the JVM, one can get decimals by using Java's built-in support.</p></section><section><h2>PHP</h2><p>PHP does not have decimals. An extension <a href="https://github.com/php-decimal/ext-decimal">exists</a> and at least one <a href="https://github.com/direvus/php-decimal">third-party library</a> exists.</p></section><section><h2>Python</h2><p>Python <a href="https://docs.python.org/3/library/decimal.html">has</a> decimals.</p></section><section><h2>Ruby</h2><p>Ruby <a href="https://ruby-doc.org/stdlib-3.1.0/libdoc/bigdecimal/rdoc/BigDecimal.html">has</a> decimals. Despite that, there is some third-party <a href="https://github.com/jgoizueta/flt">work</a> to improve the built-in support.</p></section><section><h2>Rust</h2><p>Rust does not have decimals, but a <a href="https://docs.rs/rust_decimal/latest/rust_decimal/">crate</a> exists.</p></section><section><h2>SQL</h2><p>SQL has decimals (it is the <code>DECIMAL</code> data type). (<a href="https://www.postgresql.org/docs/current/datatype-numeric.html">Here</a> is the documentation for, e.g., PostgreSQL, and <a href="https://dev.mysql.com/doc/refman/8.0/en/precision-math-decimal-characteristics.html">here</a> is the documentation for MySQL.)</p></section><section><h2>Swift</h2><p>Swift <a href="https://developer.apple.com/documentation/foundation/decimal">has</a> decimals</p></section><section><h2>TypeScript</h2><p>TypeScript does not have decimals. However, if decimals get added to JavaScript (see above), TypeScript will probably <q>inherit</q> decimals, eventually.</p></section></main>2024-04-04T12:52:09ZGetting started with Lean 4, your next programming languageurn:uuid:291db96a-5934-4c0b-97fa-3a102bdb150bLean is a language that supports proving while programming. Here‘s what I found when I first dived in, with a couple of gotchas.<main><p>I had the pleasure of learning about <a href="https://lean-lang.org/" title="Lean homepage">Lean 4</a> with <a href="https://davidchristiansen.dk/" title="David Thrane Christiansen">David Christiansen</a> and <a href="https://joachim-breitner.de/" title="Joachim Breitner‘s homepage">Joachim Breitner</a> at <a href="https://bobkonf.de/2024/breitner.html" title="Lean for the Functional Programmer">their tutorial</a> at <a href="https://bobkonf.de/2024/en/" title="BOBKonf 2024 (English version)">BOBKonf 2024</a>. I‘m planning on doing a couple of formalizations with Lean and would love to share what I learn as a total newbie, working on macOS.</p><section><h2>Needed tools</h2><p>I‘m on macOS and use Homebrew extensively. My simple go-to approach to finding new software is to do <code>brew search lean</code>. This revealed <code>lean</code> as well as surface <code>elan</code>. Running <code>brew info lean</code> showed me that that package (at the time I write this) installs Lean 3. But I know, out-of-band, that Lean 4 is what I want to work with. Running <code>brew info elan</code> looked better, but the output reminds me that (1) the information is for the <code>elan-init</code> package, not the <code>elan</code> <em>cask</em>, and (2) <code>elan-init</code> conflicts with <em>both</em> the <code>elan</code> and the aforementioned <code>lean</code>. Yikes! This strikes me as a potential problem for the community, because I think Lean 3, though it still works, is presumably not where new Lean development should be taking place. Perhaps the Homebrew formula for Lean should be updated called <q>lean3</q>, and a new <q>lean4</q> package should be made available. I‘m not sure. The situation seems less than ideal, but in short, I have been successful with the <code>elan-init</code> package.</p><p>After installing <code>elan-init</code>, you‘ll have the <code>elan</code> tool available in your shell. <code>elan</code> is the tool used for maintaining different versions of Lean, similar to <code>nvm</code> in the Node.js world or <code>pyenv</code>.</p></section><section><h2>Setting up a blank package</h2><p> </p><p>When I did the Lean 4 tutorial at BOB, I worked entirely within VS Code (…) and created a new standalone package using some in-editor functionality. At the command line, I use <code>lake init</code> to manually create a new Lean package. At first, I made the mistake of running this command, assuming it would create a new directory for me and set up any configuration and boilerplate code there. I was surprised to find, instead, that <code>lake init</code> sets things up in the <em>current</em> directory, in addition to creating a subdirectory and populating it. Using <code>lake --help</code>, I read about the <code>lake new</code> command, which does what I had in mind. So I might suggest using <code>lake new</code> rather than <code>lake init</code>.</p><p> </p><p>What‘s in the new directory? Doing <code>tree foobar</code> reveals</p><div class="highlight"><pre><code>foobar ├── Foobar │ └── Basic.lean ├── Foobar.lean ├── Main.lean ├── lakefile.lean └── lean-toolchain</code></pre></div><p> </p><p>Taking a look there, I see four <code>.lean</code> files. Here‘s what they contain:</p><p> <code>Main.lean</code></p><div class="highlight"><pre><code>import «Foobar» def main : IO Unit := IO.println s!"Hello, {hello}!"</code></pre></div><p> <code>Foobar.lean</code></p><div class="highlight"><pre><code>-- This module serves as the root of the `Foobar` library. -- Import modules here that should be built as part of the library. import «Foobar».Basic</code></pre></div><p> <code>Foobar/Basic.lean</code></p><div class="highlight"><pre><code>def hello := "world"</code></pre></div><p> <code>lakefile.lean</code></p><div class="highlight"><pre><code>import Lake open Lake DSL package «foobar» where -- add package configuration options here lean_lib «Foobar» where -- add library configuration options here @[default_target] lean_exe «foobar» where root := `Main</code></pre></div><p> </p><p>It looks like there‘s a little module structure here, and a reference to the identifier <code>hello</code>, defined in <code>Foobar/Basic.lean</code> and made available via <code>Foobar.lean</code>. I’m not going to touch <code>lakefile.lean</code> for now; as a newbie, it looks scary enough that I think I’ll just stick to things like <code>Basic.lean</code>.</p><p> </p><p>There‘s also an automatically created <code>.git</code> there, not shown in the directory output above.</p></section><section><h2>Now what?</h2><p>Now that you‘ve got Lean 4 installed and set up a package, you‘re ready to dive in to one of the official tutorials. The one I‘m working through is David‘s <a class="book" href="https://lean-lang.org/functional_programming_in_lean/">Functional Programming in Lean</a>. There‘s all sorts of additional things to learn, such as all the different <code>lake</code> commands. Enjoy!</p></section></main>2024-04-04T01:48:54Z