expm1 と log1p の紹介
このノートについて
多くのプログラミング言語（R, Python, Julia, C++, ...）では \exp(x)-1 を計算する expm1 や，\log(1+x) を計算する log1p が， exp や log とはわざわざ別に定義されています．
このような関数があることは他人から言われないとなかなか気づかないのではないかと思うのでこの記事で軽く紹介したいと思いました．私も他人のコードを見てはじめて知った記憶があります．
これらは「指数関数の部分を計算してから 1 引く」「1 足してから対数を計算する」ではなく \exp(x)-1 や log(1+x) を直接計算するので精度が高いのですが，「直接」ってどういうこと？ と思うと思うので簡単に説明します．
本文中のプログラム例は Julia です．Julia は比較的ソースを確認しやすかったので Julia を用いることにしました．
expm1
指数関数を四則演算や整数のべき乗などを使って自分で実装してみよ，と言われたとします．素朴な方法として，まずテイラー展開を使って多項式で近似する方法を考えます．
\exp(x) = 1 + x + \frac{1}{2}x^2+ \frac{1}{3!}x^3 + \frac{1}{4!}x^4 + \cdots.
有限の n 次までの多項式をプロットし，n を増やしながら GIF アニメにしてみました．
x が0に近いときは現実的な n で精度よく近似できそうです．
x が 0 に近くないときはどうするんだという問題がありますが，\log2=0.6931471805599453 を記録しておいて，次のように x = k \log 2 + r と分解すれば小さい r についての指数を計算するだけで済みます．
\begin{aligned}
\exp(x) &= \exp(k \log 2 + r)\
&= 2^k \exp(r).
\end{aligned}
ここで k は整数で，r は k \log 2 の残差です．
この考察を Julia で次の myexp のように実装してしてみます．
using Plots
n次 Taylor 多項式
function poly_n_exp(x, n)
return sum(x^k / factorial(k) for k in 0:n)
end
function myexp(x)
log2 = 0.6931471805599453
k, r = divrem(x, log2) #商の整数部分 k とあまり r
return 2^k * poly_n_exp(r, 10)
end
plot(exp, 0, 4, label="exp")
plot!(myexp, label="myexp", linestyle=:dash)
プロットをみると exp と myexp で近い値になっていることがわかります．
Julia のソース（ github.com/JuliaLang/julia/blob/master/base/speci… ）を見ると exp の実装は myexp よりもっと色々な工夫が凝らされているようですが，とりあえずここまでで「expm1 は \exp(x)-1 を直接計算する」の意味はわかります．多項式による近似の第一項は 1 なので，これを除いて計算すれば \exp(x)-1 が得られます．
\exp(x)-1 = x + \frac{1}{2}x^2+ \frac{1}{3!}x^3 + \frac{1}{4!}x^4 + \cdots.
指数関数が精度よく計算できたとしても，ほぼ 1 から 1 を引くと桁落ちが発生して 0 になってしまうことがあるので，次のような場合を比較すると expm1 の精度が高いことがわかります．
julia> exp(1e-16)-1.0
0.0
julia> expm1(1e-16)
1.0e-16
log1p
次に，対数関数を多項式で近似することを考えますが，\log(x) は x=0 で発散してしまうので， \log(1+x) を 0 の周りでテイラー展開します．
\log(1+x) = x - \frac{1}{2}x^2 + \frac{1}{3}x^3 - \frac{1}{4}x^4 + \cdots.
有限の n 次までの多項式をプロットし，n を増やしながら GIF アニメにしてみます．
0<x<1 の範囲で収束し，これも x が 0 に近いときは精度がよさそうです．
ここでもやはり x が 0 に近くないときはどうするんだという問題がありますが，次のように x = 2^k(1+r) と分解すれば小さい r について \log(1+r) を計算することで対処できます．
\begin{aligned}
\log(x) &= \log(2^k(1+r))\
&=k\log(2)+\log(1+r).
\end{aligned}
ここで k は整数です．
浮動小数点型では値を次のように符号部，仮数部，指数部にわけて保存しているので，仮数部と指数部を取り出せば k と r が得られます．
\text{値} = \text{符号部} \times \text{仮数部} \times 2^\text{指数部}
ここまでの考察を Julia で次の mylog のように実装してしてみます．
n次 Taylor 多項式
function poly_n_log1p(x, n)
return sum((-1)^(k+1) * x^k / k for k in 1:n)
end
function mylog(x)
x > 0 || throw(DomainError(x))
log2 = 0.6931471805599453
m, e = frexp(x) #仮数部と指数部
r = 2m - 1.0
k = e - 1
return k*log2 + poly_n_log1p(r, 20)
end
plot(log, 0, 4, label="log")
plot!(mylog, label="mylog", linestyle=:dash)
プロットをみると log と mylog で近い値になっていることがわかります．
これも Julia のソース（ github.com/JuliaLang/julia/blob/master/base/speci… ）を見ると，実際の log の実装はもっと複雑ですが，このように見ていくと \log(1+x) をわざわざ別の関数として実装することが自然に思えてきます．
x の絶対値が小さいときは多項式近似の poly_n_log1p を「直接」使えるからです．
次のような場合を比較すると log1p の方が精度がいいことがわかります．
julia> log(1+1e-16)
0.0
julia> log1p(1e-16)
1.0e-16
GIF アニメの作成も含めた Julia のコードはこちら：
github.com/abikoushi/Zenn_content/blob/main/jl/ex…
This month in Julia World - 2026-10
A monthly newsletter, mostly on Julia internals, digestible for casual observers. A biased, incomplete, editorialized list of what a clique of us found interesting this month, with contributions from the community.
If you want to receive the newsletter as an email, subscribe to the Community–Newsletter category on Discourse.
Please feel free to post below with your own interesting finds, or in-depth explanations, or questions about these developments.
If you would like to help with the draft for next month, please drop your short, well formatted, linked notes in this shared document. Some of it might survive by the time of posting
I am pulling back from writing these monthly newsletters for the foreseeable future, because my personal life suddenly got very busy: Like Stefan who edited the newsletter before me, I also had a baby! I hope someone, or several people, will step up to continue the newsletter.
General
Current status (as of 2026-11-01): The latest Julia release is 1.13.3, and the LTS release is 1.10.12. The master branch is at 1.15.0-DEV.318, and Julia 1.14-alpha2 is available for testing.
Julia development is accelerating. The number of opened PRs to JuliaLang/julia went from 297 in July, 282 in August (where JuliaCon took out about a week's time), 435 in September, and 752 in October. A year ago, the repo merged less than 50 commits a week, now it merges around 125. Kristoffer Carlsson alone has opened more than 100 PRs to JuliaLang/julia in October.
This is probably partially because AI agents speed up development in general, but may also be because AI agents facilitate a workflow where a developer does a deep dive into a subject and makes a spree of smaller PRs related to that subject. For this reason, some of the many changes this month is not easily summarized by single PRs that I can link to.
Core repos
- Ian Butterworth and Kristoffer Carlsson have been working hard improving latency: They have been improving significantly on the Julia performance tracker to instrument where to look. Then, they have contributed dozes of latency-reducing PRs to Julia this month. All their PRs have not yet landed, but it is already clear that Julia 1.14 will have load times, precompile times and hot-cache script run times 30-50% lower than Julia 1.10, making 1.14 the fastest Julia release by far. This has been achieved incrementally, via a large number of PRs, many improving compile times by just a few percent. There are too many PRs to list them individually, but one PR especially stands out: #63656, which cut load times by about 30%. In my opinion, Ian's and Kristoffer's efforts may result in the greatest user experience improvement in Julia since its 1.0 release in 2018.
- Jacob Quinn and Kristoffer Carlsson has brought some of the parsing infrastructure from Parsers.jl to Base Julia. This includes speeding up decimal integer parsing, hex parsing, re-implementing float parsing in Julia, and speeding up UUID parsing and Bool parsing. The new code lives in a Base.Parsers, and has an API different from Base.parse, which is still not public. The main benefit of the new API is that its failure return value tells the user what specific parsing failure occurred. This allows users to e.g. pick a wider type if integer parsing failed due to overflow.
- At JuliaCon 2025 more than a year ago, Stefan Karpinski revealed his new SAT-based package resolver. This now powers Pkg.jl. It's faster, provides pareto-optimal solutions, and gives better resolution conflict messages. It can also be upgraded later to allow resolving for other orderings, like choosing the oldest packages or optimizing for minimal download.
- Julia's installed size has grown significantly over time, from about 600 MB in Julia 1.10, to over 1,000 MB on Julia 1.13, and pushing 1,250 MB on nightly a month ago. To combat this, Kristoffer Carlsson has built a Rust CLI tool to inspect package- and system images, allowing him to see what bloats the images. He has also started tracking these sizes on perf.julialang.org. Using the tool, he has made a large number of PRs to reduce the installation size, which is now down to 668 MB on nightly. There are too many PRs to mention them all, but particularly notable changes include no longer distributing boundschecked stdlib images, and removing full debug info from the runtime.
- LLVM has been updated to v23, and support for any previous version has been dropped. LLVM 23 is slightly (perhaps 5%) faster than previous versions, and this LLVM update is among the many changes that has led to the great latency reduction in Julia this month.
- Oscar Smith is attempting to replace the trignometry functions' implementations with new ones that are both faster and more accurate. He is also attempting [the same for log functions]( julia#63547). Neither PR is merged yet, so there may be unresolved performance or correctness issues.
- Miles Cranmer has been busy modelling Julia source code in the proof assistant software Lean. It works like a kind of analytical property testing: For a method like reverse(::OrdinalRange), properties like "the input has the same number of elements as the output" are written down as lemmas together with lemmas describing its implementation, and Lean then tries to either analytically prove that the property must be correct, or else it finds a counterexample. So far, this has led to uncovering more than 400 bugs in Base (about 100 manually verified so far), and many more in packages subjected to the analysis. Miles has written a Discouse post on the subject which contains some interesting discussion. In the last few days, Miles' AI agent has begun filing issues and PRs against Julia Base: So far, 108 issues, and 107 PRs. Now, human work is needed for reviewing these PRs to make sure the AI identified the problem correctly and found the right solution. Jameson particularly has been putting in bunch of reviews, but there is still much work to be done, and you can contribute by searching for open PRs by "MilesCranmerBot", and taking stewardship of a PR.
- Julia provides green-thread concurrency through the Task type, which are under conflicting demands: One one hand, tasks must "just work", and so interact with GC and the JIT compiler, allow per-task exception handling, fork the RNG, track cancellation and much more. On the other hand, since they're, by design, the only concurrency primitive, tasks must be lightweight. The "lightweight" part has never really been achieved. Polyester.jl provides cheap threads (get it?) by spawning a small set of Tasks and reusing them. Tasks are designed to be single-use, so Polyester achieves this by reaching into Julia internals. This causes headaches: Several packages now rely on Polyester's speed, yet it breaks on every other Julia release. After yet another breakage. Valentin Churavy got fed up with this, and wrote ThreadTeams.jl, a new package that extends OhMyThreads.jl with Polyester-like cheap threads, except on more solid foundations. See also the discussion on Slack, where at least some Polyester's users are looking forward to a more stable subsitute.
- Separately, Valentin and Gabriel Baraldi are working on making Tasks faster [1, 2], but their work has not beed merged yet.
- We've had const fields in mutable structs for years now (thanks, Jameson!), but remarkably, the compiler was never updated to infer :consistent or :inaccessiblememory for const field loads. Well, Cody Tapscott fixed that.
- Julia can sometimes stack allocate Memory, but not very often, and there has long been interest in improving this. Tim Besard refactored the Memory allocation intrinsic such that the decision of whether to stack- or heap allocate happens later, which allows some LLVM optimizations to make it stack allocatable in situations it wouldn't have otherwise. Tim also teased more work on this in the future.
- Tim Besard has been submitting a series of PRs to improve RISCV support to Julia: [1, 2, 3, 4]. He has also made a large number of compiler fixes this month (about 50) which may or may not apply to RISCV. Julia currently has tier 3 support (meaning: limitied support, things may not work correctly) for Linux on RISCV.
- One major limitation of trimmed binaries right now is that external libraries need to be bundled with the binary. That means you can't just download an executable and run it - you must download a directory with the executable and a bunch of libraries. Also, the trimming process can't see which libraries your program is using, so the bundle must include all libraries in your environment. This includes chonkers ones like BLAS, even if they're not used. Gabriel Baraldi and Cody Tapscott has been working on improving the situation: Gabriel's PR allows libjulia-internal to be statically linked. Cody's (unmerged) PR allows the compiler to emit a JSON with every ccall'd library. A WIP JuliaC PR can then statically link libjulia-internal, and to remove any library not in the JSON from the bundle. Maybe in a few Julia releases, Julia apps can trimmed to single, relocatable executables?
- Gabriel Baraldi and Kristoffer Carlsson has been working on optimizing the garbage collector, contributing around 20 fixes and optimizations the last month. I don't have an overview of the overall impact of these contributions, as GC speed is not tracked on perf.julialang.org. Individual PRs showed great improvements in microbenchmarks, usually highlighting better behaviour in some pathological case. Shuhei Kadowaki also opened a PR that allows threads to share partially free pages, which should help with heap fragmentation, reducing memory usage.
- reinterpret can be used to load values of type T from an AbstractArray{S}. When used on dense arrays (like Vector), it uses unsafe_load(::Ptr{T}) internally. But the compiler has trouble tracking alias information through arbitrary pointer loads and stores: How does it know that you store into only the data part of the array and don't use the pointer to mutate the normal fields of the array, like its length? Also, using pointers require a distinct GC.@preserve for every load/store, which may hinder autovectorization. These compiler details have shown up as Base.ReinterpretArray being surprisingly slow. Andy Dienes has been working on this for some time, and now he is proposing a [new pair of builtins](unsafe_memoryrefload) which allow storing/loading a T from a MemoryRef{S}. This builtin will have special compiler support like the existing Core.memoryrefset!, and could be used to make reinterpret of arrays faster, as demonstrated by Andy in [1, 2, 3, 4]
- Julia now has functions Base.Filesystem.trylockfile and Base.Filesystem.unlockfile. The former tries to lock a file returning true if the lock could be taken, or false if it could not. This API allows files to be used as locks, which allows locks between distinct Julia processes. An example use case is a command-line program where only one instance may be running at a time.
- It was discovered that pop!(::Set) was accidentally linear instead of constant time. This was fixed by Kristoffer Carlsson by adding an extra field to Dict. It also spurred Oscar Smith to attempt a PR with a new Dict implementation, which is more similar to Python's. However, the Dict implementation is difficult to improve on because it must be fast across a wide array of usage patterns. It's also used to often throughout Base and the stdlibs that an implementation with compiles to more code may increase latency broadly across Julia, so code size must remain small. Finally, there is a lot of prior art on hash map implementations, which means there are many candidate implementations that must be considered. Oscars PR remains unmerged.
- On x86 and ARM, floating point environment ("fpenv", controlling rounding mode and which float operations cause hardware exceptions ("traps")) is crontrolled directly by the CPU via values in special registers. The OS makes sure to track fpenv per thread. Unfortunately, that doesn't work for Julia because Julia can schedule tasks on arbitrary threads and then migrate tasks between threads. That means, for example, a task may be spawned in one fpenv and then suddenly switch thread with another fpenv, causing float behaviour to spontaneously change from the point of view of the task. Even worse, user code may change the trap settings, and then execute code in the Julia runtime (e.g. the compiler), which may not handle these traps and so crashes. Jameson has pitched a PR to make Julia's runtime track fpenv per task, and to always disable trapping when running code in the Julia runtime, which should solve the issue. But there is some discussion in the PR: Perhaps having fpenv a dynamic global-ish property is just fundamentally bad, broken design, and the semantics should instead happen on a per-function level (i.e. different functions, or args controlling behaviour)? Also, do we want to make Tasks even heavier and more expensive to switch by having them track fpenv? Or maybe it's best to have Jameson's fix in Julia for now, and then discuss better fpenv design later?
- A series of PRs by Tim Besard [1, 2, 3 and probably more] adds profile-guided optimized (PGO) Julia builds to MacOS and Windows. PGO Linux builds were already supported back in 2024 thanks to Zentrik. PGO works by measuring a program's execution during a real work load. These measurements can then inform the compiler how the program should be better optimized (e.g. which functions profit from inlining, how should code be layed out in the binary, etc). The program is then re-compiled with this information, which typically produces a more optimized binary. PGO builds for 1.14 are already available from juliaup using the +opt suffixes, e.g. juliaup add alpha+opt, and may be the default builds of Julia releases in the future. PGO builds has around 10% lower compile times, and so PGO is one of the larger contributions to latency reduction for Julia 1.14.
- The implementation of === for UnionAll types is unsound due to UnionAll's layout. UnionAll is an immutable struct containing a body and a mutable TypeVar, yet === unexpectedly computed a notion of type equivalence instead of actual object identity. Not only could that lead to the contradictory result ua1 === ua2 && ua1.var != ua2.var; it also meant the compiler was free to swap/replace two UnionAll that actually had distinct layouts. Some months ago, Keno pitched a PR trying to fix this by restructuring UnionAll to a more sensible layout. Beside fixing compiler unsoundness, hopefully this will also lead to performance improvements. The PR is large, with ~9k AI-generated LOC, and with open questions of backward compatibility due to Julia's introspection, and so is being split up to smaller pieces that can be reviewed more easily [1, 2, 3].
- Tim Besard has pitched a prototype PR for computed traits in Julia. The main issue it seek to solve is Julia's monophyletic types: a fundamental problem in Julia's type system which causes heaps of practical issues. Traits has been discussed for years, and one of the main problems has been conceiving of a trait system that works well alongside the existing type system. See also Tim's brief design document.
Other community news
- TensorMixedStates.jl 2.0, a rewrite of the library, simulates closed and open quantum systems with matrix product states on top of ITensor, density matrices and Lindblad equations included.
- Christos Lillis has published a game developed in Julia called rocket plumber.
- The talks from JuliaCon 2026 are being released on YouTube now. Four videos are being released every day. You can see them on the JuliaLang YouTube account page.
- Caroll Vance has written an excellent blog post decribing how we replaced PyTorch with a Julia stack with Reactant and Enzyme. There is some discussion on Discourse, but the blog is well worth reading in its full.
60 likes
Can a constant redefinition still raise a warning?
Hello,
As I was navigating the forum about constant redefinition, I noticed that, as per 1.12 release notes:
> * Redefinition of constants is now well defined and follows world age semantics (#57253). Additional redefinitions (e.g. of types) are now allowed. See the new manual chapter on world age.
And indeed, at least in the interactive command line (REPL) of Julia 1.13, the following session "just works" (no warning):
julia> const a=1
1
julia> const a=2
2
Still, reading through the docstring of the const keyword, it states at the end:
> In some cases [bold format is mine] changing the value of a const variable gives a warning instead of an error. However, this can produce unpredictable behavior or corrupt the state of your program, and so should be avoided. This feature is intended only for convenience during interactive use.
So my question is: which are these "some cases" where redefining a const gives a warning?
Or is this text an 📜historical trace📜 of the "pre Julia 1.12 era"?
5 likes
log の計算って数表を使って実装されてるっぽいな（log(x)=log(2^k * 数表 * (1+残差)) = k log 2 + log(数表) + log(1+残差) としている？） けっこう大変
github.com/JuliaLang/julia/blob/master/base/speci…
6 likes · 262 views
@parsecranberry I wish most software was good (also, funny bug: julia#64440)
2 likes · 39 views
Julia v1.14.0-alpha2 is now available
Julia version 1.14.0-alpha2, the second alpha pre-release in the upcoming 1.14 series of releases, is now available. Check out the NEWS.md file to see what will be new in 1.14. Binaries are available via Juliaup (juliaup add 1.14) and in the upcoming release section of <julialang.org> for macOS (Intel and Apple Silicon), Windows (x86 and x86-64), glibc Linux (x86, x86-64, AArch64, RISC-V), and FreeBSD (x86-64).
As an alpha version, 1.14.0-alpha2 should not be considered production-ready. Rather, it's intended to give users, especially package developers, a chance to try out their code with 1.14.0 prior to a full release. See here for a list of commits included since 1.14.0-alpha1.
On GitHub Actions, use ~1.14.0-0 or similar to test against it (see the setup-julia action's README for options).
Optimized and assertion builds (experimental)
As with alpha1, this release also comes in optimized (+opt) and assertion (+assert) build variants; see the alpha1 announcement for details. With Juliaup:
juliaup add 1.14+opt
juliaup add 1.14+assert
Installing variants with Juliaup still requires a Juliaup release preview (juliaup self channel releasepreview followed by juliaup self update). If you try the optimized build, please report anything that behaves differently from the standard build, mentioning the variant in the issue.
17 likes
Formalizing Julia in Lean (and finding 400+ bugs in Base)
<div align="center">
Formalizing Julia in Lean
</div>
Not sure how much people have been following the ongoing cybersecurity apocalypse, but one of the interesting things I've learned from it is how exactly teams have been finding exploits. Some of these exploits are found by _formalizing_ software into Lean 4, and then attempting to prove (or refute) rigorously that certain properties are respected. This can identify problems that even the most heavy-handed prop-testing can fail to catch. Before AI coding agents, this would be a huge pain in the ass, because you literally need to write a formal math proof for every single property, but nowadays with the strong math performance of AI, it's actually possible to do this en masse for software.
I have taken a stab at modelling some of my own packages into Lean, and this has identified TONS of bugs that had gone undiscovered for a while (in DynamicExpressions.jl):
<div align="center">
</div>
Some of which seem to be problematic correctness bugs that could have been encountered silently. Now, I should also mention that I try very hard to avoid bugs in the first place (this is actually a carefully written, heavily-tested, 100%-human-reviewed codebase, not some AI slop!!) - which I want to point out to emphasize just how powerful Lean formalization is for catching bugs.
The way this works is that each Julia function gets a Lean model, and each docstring promise turns into a theorem which the agents try to prove. When any proof fails, the counterexample is usually a bug, which then gets checked against real Julia.
I have now, also, taken a stab at doing this for Julia itself - formalizing the full source code in Lean. This has also been quite fruitful: so far this has found about 400 (!) bugs in Base. I have filed 75 of the ones I manually filtered: these are the ones I thought were worth a maintainer's time, after checking each against existing issues and PRs for duplicates. Again I should emphasise that this does not mean Base is buggy relative to most software, it just means that Lean formalization is a very powerful way to catch bugs!
<div align="center">
</div>
Anyways, I thought it might be useful for others to see how this all worked, and potentially use it themselves, so I put together a repository with a writeup, and all of the Lean code I used for these:
MilesCranmer/julia-in-lean.
I discuss this more below.
---
What one of these looks like
Here is a real issue, filed as #64124. Julia reverses an ordinal range by rebuilding it with the negated step:
_reverse(r::OrdinalRange, ::Colon) = (:)(last(r), negate(step(r)), first(r))
The Lean version mirrors that line, with Julia's fixed-width integer arithmetic:
def reverse (r : Rng) : Jl Rng := do
let st ← Num.negate (step r)
colon3 (last r) st (first r)
The property, from the reverse docstring: reversing a range that Julia successfully constructed keeps the same number of elements.
def reverseCardinalityProp : Prop :=
∀ (a st b : Num) (r : Rng), stepRange a st b = .ok r →
match reverse r with
| .ok out => trueCount out = trueCount r
| .error _ => False
This property can't be proven, because it is false. The counterexample the agent found is Int8(0):typemin(Int8):typemin(Int8), which has two elements. Negating a step of -128 wraps back around to -128, so the reversed range goes from -128 "down" to 0, which is empty:
julia> r = Int8(0):typemin(Int8):typemin(Int8)
0:-128:-128
julia> length(r), length(reverse(r))
(2, 0)
The same wraparound makes sort return an empty range for some inputs, since sorting a descending range calls reverse.
Many of the bugs look like that: an edge case at typemin, an empty collection, an unsigned type. (Some of which would be hard to run into in typical use). But some are nastier:
- #64183: a miscompilation on master, where inference folds an isa check across loop iterations and a small loop returns the wrong answer. This one showed up because Markdown.rst started printing the wrong thing.
- #64147: resizing vec(M) of a BitArray corrupts M, since the two share storage.
- #64185: @sprintf of a large BigFloat after other output writes past the end of Printf's output buffer.
- #64193: an artifact path lookup can reach outside the artifact directory.
How it works
Each Julia function gets a Lean definition that follows the source line by line: same branches, same order of checks, same integer wraparound. Exceptions become values (Except JlError α, where JlError lists Julia's exception types). Then each property gets stated as a Lean Prop taken from a docstring, the manual, or an obvious invariant. Each property has to quantify over the _space_ of all inputs.
The main problem with letting agents do formal work is that they are good at producing things that look like proofs. So most of the setup checks them:
1. Differential testing first. Before proving anything, the Lean model is run on lots of inputs and compared against real Julia. For example, the integer core matched an exhaustive table of all 656,896 Int8/UInt8 cases, and the Float64 model matched on 236,954 operations. If the model disagrees with Julia, the model is wrong.
2. An audit of the build. The build fails unless every property is proven or refuted, each theorem has exactly the type of its property (or the negation), and no proof uses sorry, native_decide, or extra axioms. A separate check rejects statements that only test worked examples.
3. A refutation only counts with a reproducer. A Lean counterexample by itself is just a claim about the model. It only counts once a plain Julia script shows the same behavior on the real thing.
4. Duplicate search. Before anything is written up, the agent searches existing issues and PRs. A lot of what it finds is already known, for example #58245.
Even with all these checks, the agents can cut corners. When I moved on to proving that every @inbounds and unsafe_* access in base/ stays in bounds (1,152 sites), the first pass came back with 130 "proven" sites in under an hour. That seemed too fast... and indeed it was: a review against a fixed rubric found that 128 of those 130 proofs had just assumed the index was in bounds. The audit can't catch that, since the theorem is technically valid. So now every proof there has to pass that review too. (The memory-safety proofs are still unfinished.)
Models and cost
Everything so far has cost about $5,000 in API-equivalent usage, mostly Claude Opus 5.5 and OpenAI's Daybreak Blue (via Codex). Regular models kept refusing parts of the task, since "find overflow bugs in this source code" trips their cybersecurity filter. Daybreak Blue is meant for authorized security work, so it is less likely to refuse it (you can sign up at chatgpt.com)
Reporting
When I asked on Slack how to report these, the advice was one issue per bug rather than a single tracking issue, so that is what I do, and only for the bugs that are (1) new and (2) plausible to hit in real code. (A few people there also asked how I was finding them, which is why I wrote this up.)
I worked hard to avoid duplicates. The agent searches open and closed issues and PRs before writing anything up, and records every search. Before an issue goes up, the agent searches again, and I push back whenever something looks familiar. Many of the bugs are already known, some with a fix PR open, and I never post those. I read every issue before it goes up. The issues come from @MilesCranmerBot, which is also me (I split my GitHub activity by whether an AI wrote the text, so the provenance is easier to follow). And then any bug that might be exploitable goes to security@julialang.org instead.
All of the bugs are in the repo, including the ones I didn't post, as YAML files with a priority, the reproducer, and the output on Julia 1.13.2 and master: github.com/MilesCranmer/julia-in-lean/tree/main/j…. Most of these have not yet been reported because they are too much of an edge-case. For example, stuff like: wrong exception types, hard-to-reach edge cases, docs that contradict the code. (A handful of security-relevant ones are held back for now.)
Caveats
"Proven" means proven about the Lean model. But inevitably this model is also written by agents and checked against Julia by differential testing, not generated from Julia automatically, so a proof is only as good as the model. The bugs do not have this problem: every one has a reproducer on real Julia. Coverage is partial: parts of about 90 files in base/ plus some stdlib packages. I have also started on the C runtime (the GC, etc.). It is only about 10% done, so it is not in the repo yet.
Trying it on your own package
The repo has the DynamicExpressions.jl model as a template. I would recommend starting with one small central module, set up the differential test and the audit, and only then let agents prove things. Also, good to write down the ambiguous cases, since some "bugs" are intended behavior. When a fix is written, your agent can update the model to the new source: the same statement should now be provable, and proving it acts like a check.
Interested to hear what people think!
124 likes · 1 comment
[JuliaLang] Julia v1.14.0-alpha1 is now available
kristoffer.carlsson
October 21
Julia version 1.14.0-alpha1, the first alpha pre-release in the upcoming 1.14 series of releases, is now available. Check out the NEWS.md file to see what will be new in 1.14. Binaries are available via Juliaup (juliaup add 1.14) and in the upcoming release section of julialang.org for macOS (Intel and Apple Silicon), Windows (x86 and x86-64), glibc Linux (x86, x86-64, AArch64), and FreeBSD (x86-64).
As an alpha version, 1.14.0-alpha1 should not be considered production-ready. Rather, it’s intended to give users, especially package developers, a chance to try out their code with 1.14.0 prior to a full release.
On GitHub Actions, use ~1.14.0-0 or similar to test against it (see the setup-julia action’s README for options).
New: optimized and assertion builds (experimental)
Starting with 1.14, each release also comes in build variants made from the same sources:
- Optimized (+opt): built with profile-guided and link-time optimization, plus BOLT where supported. It is available for Windows x86-64, macOS (Intel and Apple Silicon), and Linux (x86, x86-64, AArch64). These have roughly ~10% better precompile times and load times than the standard release, but the numbers vary a bit depending on the OS and the exact packages being tested. These may at some point in the future become the default releases but for now we are keeping it conservative and requiring an opt-in.
- Assertions (+assert): Julia with its internal assertions enabled, useful when debugging Julia itself or chasing a suspected bug in it. It is available for Linux x86-64.
With Juliaup (currently, a JuliaUp release preview is required; keep reading after the commands for how to install):
juliaup add 1.14+opt
julia +1.14+opt
juliaup add 1.14+assert
The variants are also on the manual downloads page under “Optimized and assertion builds”. Installing them with Juliaup needs Juliaup 1.23, which is currently a preview release. To get it, run juliaup self channel releasepreview and then juliaup self update. In not too long the ability of using variants in the standard Juliaup release will be available.
These variants are experimental: their names and availability may change while we work out how they are published. If you try the optimized build, please report anything that behaves differently from the standard build, mentioning the variant in the issue.
Visit Topic or reply to this email to respond.
NEWS.md: github.com/JuliaLang/julia/blob/v1.14.0-alpha1/NE…
Juliaup: JuliaLang/juliaup
GitHub Actions: julia-actions/setup-julia
Julia v1.14.0-alpha1 is now available
Julia version 1.14.0-alpha1, the first alpha pre-release in the upcoming 1.14 series of releases, is now available. Check out the NEWS.md file to see what will be new in 1.14. Binaries are available via Juliaup (juliaup add 1.14) and in the upcoming release section of <julialang.org> for macOS (Intel and Apple Silicon), Windows (x86 and x86-64), glibc Linux (x86, x86-64, AArch64), and FreeBSD (x86-64).
As an alpha version, 1.14.0-alpha1 should not be considered production-ready. Rather, it's intended to give users, especially package developers, a chance to try out their code with 1.14.0 prior to a full release.
On GitHub Actions, use ~1.14.0-0 or similar to test against it (see the setup-julia action's README for options).
New: optimized and assertion builds (experimental)
Starting with 1.14, each release also comes in build variants made from the same sources:
- Optimized (+opt): built with profile-guided and link-time optimization, plus BOLT where supported. It is available for Windows x86-64, macOS (Intel and Apple Silicon), and Linux (x86, x86-64, AArch64). These have roughly ~10% better precompile times and load times than the standard release, but the numbers vary a bit depending on the OS and the exact packages being tested. These may at some point in the future become the default releases but for now we are keeping it conservative and requiring an opt-in.
- Assertions (+assert): Julia with its internal assertions enabled, useful when debugging Julia itself or chasing a suspected bug in it. It is available for Linux x86-64.
With Juliaup (currently, a JuliaUp release preview is required; keep reading after the commands for how to install):
juliaup add 1.14+opt
julia +1.14+opt
juliaup add 1.14+assert
The variants are also on the manual downloads page under "Optimized and assertion builds". Installing them with Juliaup needs Juliaup 1.23, which is currently a preview release. To get it, run juliaup self channel releasepreview and then juliaup self update. In not too long the ability of using variants in the standard Juliaup release will be available.
These variants are experimental: their names and availability may change while we work out how they are published. If you try the optimized build, please report anything that behaves differently from the standard build, mentioning the variant in the issue.
31 likes
As to (1), all the bugs Yuri filed seem to be fixed, save julia#39385, for which there is a largish PR that's still wending it's way to being merged.
All the bugs he listed as "filed by others" also seem to have been fixed, again save for one: julia#36069.
I'm not sure I understand what you're getting at with (2).
Mentions
expm1 と log1p の紹介 このノートについて 多くのプログラミング言語（R, Python, Julia, C++, ...）では \exp(x)-1 を計算する expm1 や，\log(1+x) を計算する log1p が， exp や log とはわざわざ別に定義されています． このような関数があることは他人から言われないとなかなか気づかないのではないかと思うのでこの記事で軽く紹介したいと思いました．私も他人のコードを見てはじめて知った記憶があります． これらは「指数関数の部分を計算してから 1 引く」「1 足してから対数を計算する」ではなく \exp(x)-1 や log(1+x) を直接計算するので精度が高いのですが，「直接」ってどういうこと？ と思うと思うので簡単に説明します． 本文中のプログラム例は Julia です．Julia は比較的ソースを確認しやすかったので Julia を用いることにしました． expm1 指数関数を四則演算や整数のべき乗などを使って自分で実装してみよ，と言われたとします．素朴な方法として，まずテイラー展開を使って多項式で近似する方法を考えます． \exp(x) = 1 + x + \frac{1}{2}x^2+ \frac{1}{3!}x^3 + \frac{1}{4!}x^4 + \cdots. 有限の n 次までの多項式をプロットし，n を増やしながら GIF アニメにしてみました． x が0に近いときは現実的な n で精度よく近似できそうです． x が 0 に近くないときはどうするんだという問題がありますが，\log2=0.6931471805599453 を記録しておいて，次のように x = k \log 2 + r と分解すれば小さい r についての指数を計算するだけで済みます． \begin{aligned} \exp(x) &= \exp(k \log 2 + r)\ &= 2^k \exp(r). \end{aligned} ここで k は整数で，r は k \log 2 の残差です． この考察を Julia で次の myexp のように実装してしてみます． using Plots n次 Taylor 多項式 function poly_n_exp(x, n) return sum(x^k / factorial(k) for k in 0:n) end function myexp(x) log2 = 0.6931471805599453 k, r = divrem(x, log2) #商の整数部分 k とあまり r return 2^k * poly_n_exp(r, 10) end plot(exp, 0, 4, label="exp") plot!(myexp, label="myexp", linestyle=:dash) プロットをみると exp と myexp で近い値になっていることがわかります． Julia のソース（ github.com/JuliaLang/julia/blob/master/base/speci… ）を見ると exp の実装は myexp よりもっと色々な工夫が凝らされているようですが，とりあえずここまでで「expm1 は \exp(x)-1 を直接計算する」の意味はわかります．多項式による近似の第一項は 1 なので，これを除いて計算すれば \exp(x)-1 が得られます． \exp(x)-1 = x + \frac{1}{2}x^2+ \frac{1}{3!}x^3 + \frac{1}{4!}x^4 + \cdots. 指数関数が精度よく計算できたとしても，ほぼ 1 から 1 を引くと桁落ちが発生して 0 になってしまうことがあるので，次のような場合を比較すると expm1 の精度が高いことがわかります． julia> exp(1e-16)-1.0 0.0 julia> expm1(1e-16) 1.0e-16 log1p 次に，対数関数を多項式で近似することを考えますが，\log(x) は x=0 で発散してしまうので， \log(1+x) を 0 の周りでテイラー展開します． \log(1+x) = x - \frac{1}{2}x^2 + \frac{1}{3}x^3 - \frac{1}{4}x^4 + \cdots. 有限の n 次までの多項式をプロットし，n を増やしながら GIF アニメにしてみます． 0<x<1 の範囲で収束し，これも x が 0 に近いときは精度がよさそうです． ここでもやはり x が 0 に近くないときはどうするんだという問題がありますが，次のように x = 2^k(1+r) と分解すれば小さい r について \log(1+r) を計算することで対処できます． \begin{aligned} \log(x) &= \log(2^k(1+r))\ &=k\log(2)+\log(1+r). \end{aligned} ここで k は整数です． 浮動小数点型では値を次のように符号部，仮数部，指数部にわけて保存しているので，仮数部と指数部を取り出せば k と r が得られます． \text{値} = \text{符号部} \times \text{仮数部} \times 2^\text{指数部} ここまでの考察を Julia で次の mylog のように実装してしてみます． n次 Taylor 多項式 function poly_n_log1p(x, n) return sum((-1)^(k+1) * x^k / k for k in 1:n) end function mylog(x) x > 0 || throw(DomainError(x)) log2 = 0.6931471805599453 m, e = frexp(x) #仮数部と指数部 r = 2m - 1.0 k = e - 1 return k*log2 + poly_n_log1p(r, 20) end plot(log, 0, 4, label="log") plot!(mylog, label="mylog", linestyle=:dash) プロットをみると log と mylog で近い値になっていることがわかります． これも Julia のソース（ github.com/JuliaLang/julia/blob/master/base/speci… ）を見ると，実際の log の実装はもっと複雑ですが，このように見ていくと \log(1+x) をわざわざ別の関数として実装することが自然に思えてきます． x の絶対値が小さいときは多項式近似の poly_n_log1p を「直接」使えるからです． 次のような場合を比較すると log1p の方が精度がいいことがわかります． julia> log(1+1e-16) 0.0 julia> log1p(1e-16) 1.0e-16 GIF アニメの作成も含めた Julia のコードはこちら： github.com/abikoushi/Zenn_content/blob/main/jl/ex…
This month in Julia World - 2026-10 A monthly newsletter, mostly on Julia internals, digestible for casual observers. A biased, incomplete, editorialized list of what a clique of us found interesting this month, with contributions from the community. If you want to receive the newsletter as an email, subscribe to the Community–Newsletter category on Discourse. Please feel free to post below with your own interesting finds, or in-depth explanations, or questions about these developments. If you would like to help with the draft for next month, please drop your short, well formatted, linked notes in this shared document. Some of it might survive by the time of posting I am pulling back from writing these monthly newsletters for the foreseeable future, because my personal life suddenly got very busy: Like Stefan who edited the newsletter before me, I also had a baby! I hope someone, or several people, will step up to continue the newsletter. General Current status (as of 2026-11-01): The latest Julia release is 1.13.3, and the LTS release is 1.10.12. The master branch is at 1.15.0-DEV.318, and Julia 1.14-alpha2 is available for testing. Julia development is accelerating. The number of opened PRs to JuliaLang/julia went from 297 in July, 282 in August (where JuliaCon took out about a week's time), 435 in September, and 752 in October. A year ago, the repo merged less than 50 commits a week, now it merges around 125. Kristoffer Carlsson alone has opened more than 100 PRs to JuliaLang/julia in October. This is probably partially because AI agents speed up development in general, but may also be because AI agents facilitate a workflow where a developer does a deep dive into a subject and makes a spree of smaller PRs related to that subject. For this reason, some of the many changes this month is not easily summarized by single PRs that I can link to. Core repos - Ian Butterworth and Kristoffer Carlsson have been working hard improving latency: They have been improving significantly on the Julia performance tracker to instrument where to look. Then, they have contributed dozes of latency-reducing PRs to Julia this month. All their PRs have not yet landed, but it is already clear that Julia 1.14 will have load times, precompile times and hot-cache script run times 30-50% lower than Julia 1.10, making 1.14 the fastest Julia release by far. This has been achieved incrementally, via a large number of PRs, many improving compile times by just a few percent. There are too many PRs to list them individually, but one PR especially stands out: #63656, which cut load times by about 30%. In my opinion, Ian's and Kristoffer's efforts may result in the greatest user experience improvement in Julia since its 1.0 release in 2018. - Jacob Quinn and Kristoffer Carlsson has brought some of the parsing infrastructure from Parsers.jl to Base Julia. This includes speeding up decimal integer parsing, hex parsing, re-implementing float parsing in Julia, and speeding up UUID parsing and Bool parsing. The new code lives in a Base.Parsers, and has an API different from Base.parse, which is still not public. The main benefit of the new API is that its failure return value tells the user what specific parsing failure occurred. This allows users to e.g. pick a wider type if integer parsing failed due to overflow. - At JuliaCon 2025 more than a year ago, Stefan Karpinski revealed his new SAT-based package resolver. This now powers Pkg.jl. It's faster, provides pareto-optimal solutions, and gives better resolution conflict messages. It can also be upgraded later to allow resolving for other orderings, like choosing the oldest packages or optimizing for minimal download. - Julia's installed size has grown significantly over time, from about 600 MB in Julia 1.10, to over 1,000 MB on Julia 1.13, and pushing 1,250 MB on nightly a month ago. To combat this, Kristoffer Carlsson has built a Rust CLI tool to inspect package- and system images, allowing him to see what bloats the images. He has also started tracking these sizes on perf.julialang.org. Using the tool, he has made a large number of PRs to reduce the installation size, which is now down to 668 MB on nightly. There are too many PRs to mention them all, but particularly notable changes include no longer distributing boundschecked stdlib images, and removing full debug info from the runtime. - LLVM has been updated to v23, and support for any previous version has been dropped. LLVM 23 is slightly (perhaps 5%) faster than previous versions, and this LLVM update is among the many changes that has led to the great latency reduction in Julia this month. - Oscar Smith is attempting to replace the trignometry functions' implementations with new ones that are both faster and more accurate. He is also attempting [the same for log functions]( julia#63547). Neither PR is merged yet, so there may be unresolved performance or correctness issues. - Miles Cranmer has been busy modelling Julia source code in the proof assistant software Lean. It works like a kind of analytical property testing: For a method like reverse(::OrdinalRange), properties like "the input has the same number of elements as the output" are written down as lemmas together with lemmas describing its implementation, and Lean then tries to either analytically prove that the property must be correct, or else it finds a counterexample. So far, this has led to uncovering more than 400 bugs in Base (about 100 manually verified so far), and many more in packages subjected to the analysis. Miles has written a Discouse post on the subject which contains some interesting discussion. In the last few days, Miles' AI agent has begun filing issues and PRs against Julia Base: So far, 108 issues, and 107 PRs. Now, human work is needed for reviewing these PRs to make sure the AI identified the problem correctly and found the right solution. Jameson particularly has been putting in bunch of reviews, but there is still much work to be done, and you can contribute by searching for open PRs by "MilesCranmerBot", and taking stewardship of a PR. - Julia provides green-thread concurrency through the Task type, which are under conflicting demands: One one hand, tasks must "just work", and so interact with GC and the JIT compiler, allow per-task exception handling, fork the RNG, track cancellation and much more. On the other hand, since they're, by design, the only concurrency primitive, tasks must be lightweight. The "lightweight" part has never really been achieved. Polyester.jl provides cheap threads (get it?) by spawning a small set of Tasks and reusing them. Tasks are designed to be single-use, so Polyester achieves this by reaching into Julia internals. This causes headaches: Several packages now rely on Polyester's speed, yet it breaks on every other Julia release. After yet another breakage. Valentin Churavy got fed up with this, and wrote ThreadTeams.jl, a new package that extends OhMyThreads.jl with Polyester-like cheap threads, except on more solid foundations. See also the discussion on Slack, where at least some Polyester's users are looking forward to a more stable subsitute. - Separately, Valentin and Gabriel Baraldi are working on making Tasks faster [1, 2], but their work has not beed merged yet. - We've had const fields in mutable structs for years now (thanks, Jameson!), but remarkably, the compiler was never updated to infer :consistent or :inaccessiblememory for const field loads. Well, Cody Tapscott fixed that. - Julia can sometimes stack allocate Memory, but not very often, and there has long been interest in improving this. Tim Besard refactored the Memory allocation intrinsic such that the decision of whether to stack- or heap allocate happens later, which allows some LLVM optimizations to make it stack allocatable in situations it wouldn't have otherwise. Tim also teased more work on this in the future. - Tim Besard has been submitting a series of PRs to improve RISCV support to Julia: [1, 2, 3, 4]. He has also made a large number of compiler fixes this month (about 50) which may or may not apply to RISCV. Julia currently has tier 3 support (meaning: limitied support, things may not work correctly) for Linux on RISCV. - One major limitation of trimmed binaries right now is that external libraries need to be bundled with the binary. That means you can't just download an executable and run it - you must download a directory with the executable and a bunch of libraries. Also, the trimming process can't see which libraries your program is using, so the bundle must include all libraries in your environment. This includes chonkers ones like BLAS, even if they're not used. Gabriel Baraldi and Cody Tapscott has been working on improving the situation: Gabriel's PR allows libjulia-internal to be statically linked. Cody's (unmerged) PR allows the compiler to emit a JSON with every ccall'd library. A WIP JuliaC PR can then statically link libjulia-internal, and to remove any library not in the JSON from the bundle. Maybe in a few Julia releases, Julia apps can trimmed to single, relocatable executables? - Gabriel Baraldi and Kristoffer Carlsson has been working on optimizing the garbage collector, contributing around 20 fixes and optimizations the last month. I don't have an overview of the overall impact of these contributions, as GC speed is not tracked on perf.julialang.org. Individual PRs showed great improvements in microbenchmarks, usually highlighting better behaviour in some pathological case. Shuhei Kadowaki also opened a PR that allows threads to share partially free pages, which should help with heap fragmentation, reducing memory usage. - reinterpret can be used to load values of type T from an AbstractArray{S}. When used on dense arrays (like Vector), it uses unsafe_load(::Ptr{T}) internally. But the compiler has trouble tracking alias information through arbitrary pointer loads and stores: How does it know that you store into only the data part of the array and don't use the pointer to mutate the normal fields of the array, like its length? Also, using pointers require a distinct GC.@preserve for every load/store, which may hinder autovectorization. These compiler details have shown up as Base.ReinterpretArray being surprisingly slow. Andy Dienes has been working on this for some time, and now he is proposing a [new pair of builtins](unsafe_memoryrefload) which allow storing/loading a T from a MemoryRef{S}. This builtin will have special compiler support like the existing Core.memoryrefset!, and could be used to make reinterpret of arrays faster, as demonstrated by Andy in [1, 2, 3, 4] - Julia now has functions Base.Filesystem.trylockfile and Base.Filesystem.unlockfile. The former tries to lock a file returning true if the lock could be taken, or false if it could not. This API allows files to be used as locks, which allows locks between distinct Julia processes. An example use case is a command-line program where only one instance may be running at a time. - It was discovered that pop!(::Set) was accidentally linear instead of constant time. This was fixed by Kristoffer Carlsson by adding an extra field to Dict. It also spurred Oscar Smith to attempt a PR with a new Dict implementation, which is more similar to Python's. However, the Dict implementation is difficult to improve on because it must be fast across a wide array of usage patterns. It's also used to often throughout Base and the stdlibs that an implementation with compiles to more code may increase latency broadly across Julia, so code size must remain small. Finally, there is a lot of prior art on hash map implementations, which means there are many candidate implementations that must be considered. Oscars PR remains unmerged. - On x86 and ARM, floating point environment ("fpenv", controlling rounding mode and which float operations cause hardware exceptions ("traps")) is crontrolled directly by the CPU via values in special registers. The OS makes sure to track fpenv per thread. Unfortunately, that doesn't work for Julia because Julia can schedule tasks on arbitrary threads and then migrate tasks between threads. That means, for example, a task may be spawned in one fpenv and then suddenly switch thread with another fpenv, causing float behaviour to spontaneously change from the point of view of the task. Even worse, user code may change the trap settings, and then execute code in the Julia runtime (e.g. the compiler), which may not handle these traps and so crashes. Jameson has pitched a PR to make Julia's runtime track fpenv per task, and to always disable trapping when running code in the Julia runtime, which should solve the issue. But there is some discussion in the PR: Perhaps having fpenv a dynamic global-ish property is just fundamentally bad, broken design, and the semantics should instead happen on a per-function level (i.e. different functions, or args controlling behaviour)? Also, do we want to make Tasks even heavier and more expensive to switch by having them track fpenv? Or maybe it's best to have Jameson's fix in Julia for now, and then discuss better fpenv design later? - A series of PRs by Tim Besard [1, 2, 3 and probably more] adds profile-guided optimized (PGO) Julia builds to MacOS and Windows. PGO Linux builds were already supported back in 2024 thanks to Zentrik. PGO works by measuring a program's execution during a real work load. These measurements can then inform the compiler how the program should be better optimized (e.g. which functions profit from inlining, how should code be layed out in the binary, etc). The program is then re-compiled with this information, which typically produces a more optimized binary. PGO builds for 1.14 are already available from juliaup using the +opt suffixes, e.g. juliaup add alpha+opt, and may be the default builds of Julia releases in the future. PGO builds has around 10% lower compile times, and so PGO is one of the larger contributions to latency reduction for Julia 1.14. - The implementation of === for UnionAll types is unsound due to UnionAll's layout. UnionAll is an immutable struct containing a body and a mutable TypeVar, yet === unexpectedly computed a notion of type equivalence instead of actual object identity. Not only could that lead to the contradictory result ua1 === ua2 && ua1.var != ua2.var; it also meant the compiler was free to swap/replace two UnionAll that actually had distinct layouts. Some months ago, Keno pitched a PR trying to fix this by restructuring UnionAll to a more sensible layout. Beside fixing compiler unsoundness, hopefully this will also lead to performance improvements. The PR is large, with ~9k AI-generated LOC, and with open questions of backward compatibility due to Julia's introspection, and so is being split up to smaller pieces that can be reviewed more easily [1, 2, 3]. - Tim Besard has pitched a prototype PR for computed traits in Julia. The main issue it seek to solve is Julia's monophyletic types: a fundamental problem in Julia's type system which causes heaps of practical issues. Traits has been discussed for years, and one of the main problems has been conceiving of a trait system that works well alongside the existing type system. See also Tim's brief design document. Other community news - TensorMixedStates.jl 2.0, a rewrite of the library, simulates closed and open quantum systems with matrix product states on top of ITensor, density matrices and Lindblad equations included. - Christos Lillis has published a game developed in Julia called rocket plumber. - The talks from JuliaCon 2026 are being released on YouTube now. Four videos are being released every day. You can see them on the JuliaLang YouTube account page. - Caroll Vance has written an excellent blog post decribing how we replaced PyTorch with a Julia stack with Reactant and Enzyme. There is some discussion on Discourse, but the blog is well worth reading in its full.
Can a constant redefinition still raise a warning? Hello, As I was navigating the forum about constant redefinition, I noticed that, as per 1.12 release notes: > * Redefinition of constants is now well defined and follows world age semantics (#57253). Additional redefinitions (e.g. of types) are now allowed. See the new manual chapter on world age. And indeed, at least in the interactive command line (REPL) of Julia 1.13, the following session "just works" (no warning): julia> const a=1 1 julia> const a=2 2 Still, reading through the docstring of the const keyword, it states at the end: > In some cases [bold format is mine] changing the value of a const variable gives a warning instead of an error. However, this can produce unpredictable behavior or corrupt the state of your program, and so should be avoided. This feature is intended only for convenience during interactive use. So my question is: which are these "some cases" where redefining a const gives a warning? Or is this text an 📜historical trace📜 of the "pre Julia 1.12 era"?
log の計算って数表を使って実装されてるっぽいな（log(x)=log(2^k * 数表 * (1+残差)) = k log 2 + log(数表) + log(1+残差) としている？） けっこう大変 github.com/JuliaLang/julia/blob/master/base/speci…
@parsecranberry I wish most software was good (also, funny bug: julia#64440)
Julia v1.14.0-alpha2 is now available Julia version 1.14.0-alpha2, the second alpha pre-release in the upcoming 1.14 series of releases, is now available. Check out the NEWS.md file to see what will be new in 1.14. Binaries are available via Juliaup (juliaup add 1.14) and in the upcoming release section of <julialang.org> for macOS (Intel and Apple Silicon), Windows (x86 and x86-64), glibc Linux (x86, x86-64, AArch64, RISC-V), and FreeBSD (x86-64). As an alpha version, 1.14.0-alpha2 should not be considered production-ready. Rather, it's intended to give users, especially package developers, a chance to try out their code with 1.14.0 prior to a full release. See here for a list of commits included since 1.14.0-alpha1. On GitHub Actions, use ~1.14.0-0 or similar to test against it (see the setup-julia action's README for options). Optimized and assertion builds (experimental) As with alpha1, this release also comes in optimized (+opt) and assertion (+assert) build variants; see the alpha1 announcement for details. With Juliaup: juliaup add 1.14+opt juliaup add 1.14+assert Installing variants with Juliaup still requires a Juliaup release preview (juliaup self channel releasepreview followed by juliaup self update). If you try the optimized build, please report anything that behaves differently from the standard build, mentioning the variant in the issue.
Formalizing Julia in Lean (and finding 400+ bugs in Base) <div align="center"> Formalizing Julia in Lean </div> Not sure how much people have been following the ongoing cybersecurity apocalypse, but one of the interesting things I've learned from it is how exactly teams have been finding exploits. Some of these exploits are found by _formalizing_ software into Lean 4, and then attempting to prove (or refute) rigorously that certain properties are respected. This can identify problems that even the most heavy-handed prop-testing can fail to catch. Before AI coding agents, this would be a huge pain in the ass, because you literally need to write a formal math proof for every single property, but nowadays with the strong math performance of AI, it's actually possible to do this en masse for software. I have taken a stab at modelling some of my own packages into Lean, and this has identified TONS of bugs that had gone undiscovered for a while (in DynamicExpressions.jl): <div align="center">  </div> Some of which seem to be problematic correctness bugs that could have been encountered silently. Now, I should also mention that I try very hard to avoid bugs in the first place (this is actually a carefully written, heavily-tested, 100%-human-reviewed codebase, not some AI slop!!) - which I want to point out to emphasize just how powerful Lean formalization is for catching bugs. The way this works is that each Julia function gets a Lean model, and each docstring promise turns into a theorem which the agents try to prove. When any proof fails, the counterexample is usually a bug, which then gets checked against real Julia. I have now, also, taken a stab at doing this for Julia itself - formalizing the full source code in Lean. This has also been quite fruitful: so far this has found about 400 (!) bugs in Base. I have filed 75 of the ones I manually filtered: these are the ones I thought were worth a maintainer's time, after checking each against existing issues and PRs for duplicates. Again I should emphasise that this does not mean Base is buggy relative to most software, it just means that Lean formalization is a very powerful way to catch bugs! <div align="center">  </div> Anyways, I thought it might be useful for others to see how this all worked, and potentially use it themselves, so I put together a repository with a writeup, and all of the Lean code I used for these: MilesCranmer/julia-in-lean. I discuss this more below. --- What one of these looks like Here is a real issue, filed as #64124. Julia reverses an ordinal range by rebuilding it with the negated step: _reverse(r::OrdinalRange, ::Colon) = (:)(last(r), negate(step(r)), first(r)) The Lean version mirrors that line, with Julia's fixed-width integer arithmetic: def reverse (r : Rng) : Jl Rng := do let st ← Num.negate (step r) colon3 (last r) st (first r) The property, from the reverse docstring: reversing a range that Julia successfully constructed keeps the same number of elements. def reverseCardinalityProp : Prop := ∀ (a st b : Num) (r : Rng), stepRange a st b = .ok r → match reverse r with | .ok out => trueCount out = trueCount r | .error _ => False This property can't be proven, because it is false. The counterexample the agent found is Int8(0):typemin(Int8):typemin(Int8), which has two elements. Negating a step of -128 wraps back around to -128, so the reversed range goes from -128 "down" to 0, which is empty: julia> r = Int8(0):typemin(Int8):typemin(Int8) 0:-128:-128 julia> length(r), length(reverse(r)) (2, 0) The same wraparound makes sort return an empty range for some inputs, since sorting a descending range calls reverse. Many of the bugs look like that: an edge case at typemin, an empty collection, an unsigned type. (Some of which would be hard to run into in typical use). But some are nastier: - #64183: a miscompilation on master, where inference folds an isa check across loop iterations and a small loop returns the wrong answer. This one showed up because Markdown.rst started printing the wrong thing. - #64147: resizing vec(M) of a BitArray corrupts M, since the two share storage. - #64185: @sprintf of a large BigFloat after other output writes past the end of Printf's output buffer. - #64193: an artifact path lookup can reach outside the artifact directory. How it works Each Julia function gets a Lean definition that follows the source line by line: same branches, same order of checks, same integer wraparound. Exceptions become values (Except JlError α, where JlError lists Julia's exception types). Then each property gets stated as a Lean Prop taken from a docstring, the manual, or an obvious invariant. Each property has to quantify over the _space_ of all inputs. The main problem with letting agents do formal work is that they are good at producing things that look like proofs. So most of the setup checks them: 1. Differential testing first. Before proving anything, the Lean model is run on lots of inputs and compared against real Julia. For example, the integer core matched an exhaustive table of all 656,896 Int8/UInt8 cases, and the Float64 model matched on 236,954 operations. If the model disagrees with Julia, the model is wrong. 2. An audit of the build. The build fails unless every property is proven or refuted, each theorem has exactly the type of its property (or the negation), and no proof uses sorry, native_decide, or extra axioms. A separate check rejects statements that only test worked examples. 3. A refutation only counts with a reproducer. A Lean counterexample by itself is just a claim about the model. It only counts once a plain Julia script shows the same behavior on the real thing. 4. Duplicate search. Before anything is written up, the agent searches existing issues and PRs. A lot of what it finds is already known, for example #58245. Even with all these checks, the agents can cut corners. When I moved on to proving that every @inbounds and unsafe_* access in base/ stays in bounds (1,152 sites), the first pass came back with 130 "proven" sites in under an hour. That seemed too fast... and indeed it was: a review against a fixed rubric found that 128 of those 130 proofs had just assumed the index was in bounds. The audit can't catch that, since the theorem is technically valid. So now every proof there has to pass that review too. (The memory-safety proofs are still unfinished.) Models and cost Everything so far has cost about $5,000 in API-equivalent usage, mostly Claude Opus 5.5 and OpenAI's Daybreak Blue (via Codex). Regular models kept refusing parts of the task, since "find overflow bugs in this source code" trips their cybersecurity filter. Daybreak Blue is meant for authorized security work, so it is less likely to refuse it (you can sign up at chatgpt.com) Reporting When I asked on Slack how to report these, the advice was one issue per bug rather than a single tracking issue, so that is what I do, and only for the bugs that are (1) new and (2) plausible to hit in real code. (A few people there also asked how I was finding them, which is why I wrote this up.) I worked hard to avoid duplicates. The agent searches open and closed issues and PRs before writing anything up, and records every search. Before an issue goes up, the agent searches again, and I push back whenever something looks familiar. Many of the bugs are already known, some with a fix PR open, and I never post those. I read every issue before it goes up. The issues come from @MilesCranmerBot, which is also me (I split my GitHub activity by whether an AI wrote the text, so the provenance is easier to follow). And then any bug that might be exploitable goes to security@julialang.org instead. All of the bugs are in the repo, including the ones I didn't post, as YAML files with a priority, the reproducer, and the output on Julia 1.13.2 and master: github.com/MilesCranmer/julia-in-lean/tree/main/j…. Most of these have not yet been reported because they are too much of an edge-case. For example, stuff like: wrong exception types, hard-to-reach edge cases, docs that contradict the code. (A handful of security-relevant ones are held back for now.) Caveats "Proven" means proven about the Lean model. But inevitably this model is also written by agents and checked against Julia by differential testing, not generated from Julia automatically, so a proof is only as good as the model. The bugs do not have this problem: every one has a reproducer on real Julia. Coverage is partial: parts of about 90 files in base/ plus some stdlib packages. I have also started on the C runtime (the GC, etc.). It is only about 10% done, so it is not in the repo yet. Trying it on your own package The repo has the DynamicExpressions.jl model as a template. I would recommend starting with one small central module, set up the differential test and the audit, and only then let agents prove things. Also, good to write down the ambiguous cases, since some "bugs" are intended behavior. When a fix is written, your agent can update the model to the new source: the same statement should now be provable, and proving it acts like a check. Interested to hear what people think!
[JuliaLang] Julia v1.14.0-alpha1 is now available kristoffer.carlsson October 21 Julia version 1.14.0-alpha1, the first alpha pre-release in the upcoming 1.14 series of releases, is now available. Check out the NEWS.md file to see what will be new in 1.14. Binaries are available via Juliaup (juliaup add 1.14) and in the upcoming release section of julialang.org for macOS (Intel and Apple Silicon), Windows (x86 and x86-64), glibc Linux (x86, x86-64, AArch64), and FreeBSD (x86-64). As an alpha version, 1.14.0-alpha1 should not be considered production-ready. Rather, it’s intended to give users, especially package developers, a chance to try out their code with 1.14.0 prior to a full release. On GitHub Actions, use ~1.14.0-0 or similar to test against it (see the setup-julia action’s README for options). New: optimized and assertion builds (experimental) Starting with 1.14, each release also comes in build variants made from the same sources: - Optimized (+opt): built with profile-guided and link-time optimization, plus BOLT where supported. It is available for Windows x86-64, macOS (Intel and Apple Silicon), and Linux (x86, x86-64, AArch64). These have roughly ~10% better precompile times and load times than the standard release, but the numbers vary a bit depending on the OS and the exact packages being tested. These may at some point in the future become the default releases but for now we are keeping it conservative and requiring an opt-in. - Assertions (+assert): Julia with its internal assertions enabled, useful when debugging Julia itself or chasing a suspected bug in it. It is available for Linux x86-64. With Juliaup (currently, a JuliaUp release preview is required; keep reading after the commands for how to install): juliaup add 1.14+opt julia +1.14+opt juliaup add 1.14+assert The variants are also on the manual downloads page under “Optimized and assertion builds”. Installing them with Juliaup needs Juliaup 1.23, which is currently a preview release. To get it, run juliaup self channel releasepreview and then juliaup self update. In not too long the ability of using variants in the standard Juliaup release will be available. These variants are experimental: their names and availability may change while we work out how they are published. If you try the optimized build, please report anything that behaves differently from the standard build, mentioning the variant in the issue. Visit Topic or reply to this email to respond. NEWS.md: github.com/JuliaLang/julia/blob/v1.14.0-alpha1/NE… Juliaup: JuliaLang/juliaup GitHub Actions: julia-actions/setup-julia
Julia v1.14.0-alpha1 is now available Julia version 1.14.0-alpha1, the first alpha pre-release in the upcoming 1.14 series of releases, is now available. Check out the NEWS.md file to see what will be new in 1.14. Binaries are available via Juliaup (juliaup add 1.14) and in the upcoming release section of <julialang.org> for macOS (Intel and Apple Silicon), Windows (x86 and x86-64), glibc Linux (x86, x86-64, AArch64), and FreeBSD (x86-64). As an alpha version, 1.14.0-alpha1 should not be considered production-ready. Rather, it's intended to give users, especially package developers, a chance to try out their code with 1.14.0 prior to a full release. On GitHub Actions, use ~1.14.0-0 or similar to test against it (see the setup-julia action's README for options). New: optimized and assertion builds (experimental) Starting with 1.14, each release also comes in build variants made from the same sources: - Optimized (+opt): built with profile-guided and link-time optimization, plus BOLT where supported. It is available for Windows x86-64, macOS (Intel and Apple Silicon), and Linux (x86, x86-64, AArch64). These have roughly ~10% better precompile times and load times than the standard release, but the numbers vary a bit depending on the OS and the exact packages being tested. These may at some point in the future become the default releases but for now we are keeping it conservative and requiring an opt-in. - Assertions (+assert): Julia with its internal assertions enabled, useful when debugging Julia itself or chasing a suspected bug in it. It is available for Linux x86-64. With Juliaup (currently, a JuliaUp release preview is required; keep reading after the commands for how to install): juliaup add 1.14+opt julia +1.14+opt juliaup add 1.14+assert The variants are also on the manual downloads page under "Optimized and assertion builds". Installing them with Juliaup needs Juliaup 1.23, which is currently a preview release. To get it, run juliaup self channel releasepreview and then juliaup self update. In not too long the ability of using variants in the standard Juliaup release will be available. These variants are experimental: their names and availability may change while we work out how they are published. If you try the optimized build, please report anything that behaves differently from the standard build, mentioning the variant in the issue.
As to (1), all the bugs Yuri filed seem to be fixed, save julia#39385, for which there is a largish PR that's still wending it's way to being merged. All the bugs he listed as "filed by others" also seem to have been fixed, again save for one: julia#36069. I'm not sure I understand what you're getting at with (2).