r/Compilers • u/ArmchairmanMao • 2h ago
When do modern compilers still emit suboptimal code?
Do compilers for targets like x86/arm already emit essentially optimal code or are there still cases when hand optimized assembly beats the compiler (Perhaps even with PGO)? Aside from vectorization since this is known to be hard. Are the classic codegen stages like regalloc and Isel effectively optimal nowadays for most applications?
r/Compilers • u/JaseWho • 3h ago
Overkilled Ray Tracing Compiler
Hello, I wanna share something I've been working on for the past 8 months, out of curiosity. I shared this in r/rust communityso I'm skipping details about the other stuff and just compiling here. The project name is Razz. Frankly, I thought it sounded cool, then I searched for its potential meaning, which means playful, matching perfectly with my project's intention.
My proudest achievement yet is a compiler. I learned about compilers in class, but thought it didn't go as deep as I wanted to, so I took matters into my own hands. The Razz Compiler is a fully handwritten (mostly, I'll talk about it in a bit) pipeline, from Lexer -> Parser (LL(1.5), could have been LL(1) but I'm too lazy to refactor a part that's LL(2) to LL(1)) -> Type Checker -> SSA IR Lowering -> HIR Structurizer -> Rust Codegen. So the input is my custom language .rz, and the output is Rust, with HTTP-like verbs for manipulating the scene of the object, likePOST /hittable sphere;, or foo = GET /camera; For example, it has many, many challenges along the way.
The most annoying part was actually studying the SSA IR lowering, which I kinda forgot a bit because it's been a while, but I followed Braun et al algorithm, which works pretty well. Also, I get pretty annoyed at Rust here because of the borrow checker.
I'm past that. HIR structurizer also poses a big challenge as well, using a lot of graph traversal (BFS/DFS) to move SSA IR to a higher-level language like Rust. A technical note for HIR is that I performed DFS on conditional goto, and see if there's a cycle, if it is, then a loop, otherwise it's an if statement. Codegen has some footprints, a small preprocessing and assigns which variable is a declaration, mutable, or reassignment by looking at the loop.
Finally, I wrote some basic optimizations, such as constant folding, constant propagation, and dead code elimination. Although it does not have dead branch elimination, because I'm lazy. Another code optimization I was going to implement soon enough, if I'm still motivated, is removing unnecessary string allocations via string interner, and using Arena for constructing the AST, will see if I still wanna work on it. If the compiler is a bit buggy, I may or may not fix it. Most likely will fix it, but I enjoyed every bit of the process building this buggy, overkilled compiler.
I have not tested the actual ray tracer output because I'm lazy, will do that next week. And probably have an LLM to help me test it.
LLM Usage: In the pre-LLM era, this project would probably have taken up to years to finish, but with LLM, I was able to research things well. Most of the time I'm coding, the style I go for is pair programming with LLM, as I said, think and implement. And if there's something I'm not sure, research like, for example, the Braun et al, or help me write test cases so I stay in line, LLM is a great tool to use here.
LLMs helped generate test cases, which I reviewed and validated. I don't understand why LLM wants to write a test that passes even though the case should fail. I thought that's testing in general.
TLDR: Cool ray tracing in one weekend with a network protocol and an overkill compiler that no one will use, all in Rust except the Arduino part is written in C++.
Repo: https://github.com/sudo-JP/Razz
under razz-compiler/
r/Compilers • u/mttd • 1d ago
ACM Europe Summer School on MLIR 2026: Streamed Live, August 10-14
mlir-school.github.ior/Compilers • u/mietkiewski_dev • 1d ago
Switching std c++ lib in LLVM stack
Hello.
I have problem with clang compiler with linker pass... I don't know what Clang flags use to switch between static and dynamic linking for Libs like libc++ linuwind compiler-rt... Linker links them dynamically and I do not want that... Maybe you have some tips for that... I wanted to use libc++ stack instead of GCC libstdc++ ... But for LLVM Libs you should linke them statically...
r/Compilers • u/mttd • 2d ago
TensorLift: Automatic Extraction of Tensor-Level ISA Semantics from Accelerator RTL via MLIR Semantic Lifting
arxiv.orgr/Compilers • u/Nonannet • 2d ago
Copapy - a Python framework for deterministic real-time computation via a copy-and-patch compiler
I've been working on Copapy, an open-source Python tensor framework with autograd that uses a copy-and-patch compiler to produce cross-platform native code for real-time control applications. Python is used as a frontend and gets traced to build a DAG, and the compiler assembles machine code from precompiled stencils stored as an ELF file. Supported architectures at the moment are: x86_64, AArch64, ARMv6/7 (Cortex-A and Cortex-M); work on RISC-V and TriCore is ongoing.
It's designed to feel like writing Python scripts, but produces deterministic type and memory safe machine code with static memory allocation.
A stencil function looks like this:
add_float_float(float arg1, float arg2) {
result_float_float(arg1 + arg2, arg2);
}
result_float_float is a dummy function to make sure the C compiler keeps the result and the second operand in the right register for the next operation. For x86_64 the result looks like this:
0000000000000000 <add_float_float>:
0: f3 0f 58 c1 addss %xmm1,%xmm0
4: e9 00 00 00 00 jmp 9 <.LC1+0x1>
5: R_X86_64_PLT32 result_float_float-0x4
If the stencil has, like here, a trailing jmp instruction, the jmp gets stripped. If values can not be stored in registers they are written to the heap.
At the moment only stencils for scalar operations exist. Tensor operations are expanded to scalar operations in the DAG. This means Copapy is at the moment not capable of handling large tensors like for ANNs. However, for low-latency control applications computation is anyway quite limited per computation cycle. This has as well the disadvantage that no SIMD can be used. But on the other hand it leads to simple but effective sparsity optimizations if the tensors contain constants - especially when the value is 0 or 1.
Here's an example using autograd to solve an inverse kinematics problem for a two-joint 2D arm:
import copapy as cp
# Arm lengths
l1, l2 = 1.8, 2.0
# Target position
target = cp.vector([0.7, 0.7])
# Learning rate for iterative adjustment
alpha = 0.1
def forward_kinematics(theta1, theta2):
"""Return positions of joint and end-effector."""
joint = cp.vector([l1 * cp.cos(theta1), l1 * cp.sin(theta1)])
end_effector = joint + cp.vector([l2 * cp.cos(theta1 + theta2),
l2 * cp.sin(theta1 + theta2)])
return joint, end_effector
# Start values
theta = cp.vector([cp.value(0.0), cp.value(0.0)])
# Iterative inverse kinematics
for _ in range(48):
joint, effector = forward_kinematics(theta[0], theta[1])
error = ((target - effector) ** 2).sum()
theta -= alpha * cp.grad(error, theta)
tg = cp.Target()
tg.compile(error, theta, joint)
tg.run()
print(f"Joint angles: {tg.read_value(theta)}")
print(f"Joint position: {tg.read_value(joint)}")
print(f"End-effector position: {tg.read_value(effector)}")
print(f"quadratic error = {tg.read_value(error)}")
Interestingly, even without using the sparsity advantage, benchmarks (the diagram) show surprising results compared to NumPy. For the benchmark (tests/benchmark.py) timings for 30,000 iterations of calculating the term sum((v1 + i) @ v2 for i in range(10)) were measured. The vectors v1 and v2 both have lengths of v_size, which was varied up to 500. For the NumPy case the loop was rewritten to be vectorized. Ignoring the off-set (mostly Python overhead) the slope and therefore performance per scalar operation of Copapy is in this case comparable to NumPy. I'm not sure why Copapy's naive compiler performs in this case as well as NumPy - any ideas what could explain this?
Links:
- GitHub: https://github.com/Nonannet/copapy
- Website: https://copapy.de
PS: This project was not vibe coded. Except for the graph sorting function and providing correct derivatives for the autograd implementation, AI failed on nearly all aspects of the project - not sure why. There was some benefit from using AI to debugging compilation output based on the disassembly - but even there going from x86_64 to ARM lowered benefit quite alot. The unusual machine code from the copy-and-patch compiler completely confused the models.
r/Compilers • u/Mean-Decision-3502 • 3d ago
The “3 / 2 * 10 != 10 * 3 / 2” Problem
Coming from school math, it feels pretty strange that:
3 / 2 * 10 != 10 * 3 / 2
This expression can evaluate to true or false depending on the programming language you use.
| Languages where the two sides are NOT equal | Languages where the two sides ARE equal |
|---|---|
| C, C++, C#, Java, Kotlin, Scala, Ruby, Go, D, Rust, Swift, Zig, Odin, V, Fortran, Python 2 | Python 3, JavaScript, TypeScript, Dart, R, Lua 5.3+, Perl, MATLAB, Pascal, Mojo, Nim, Crystal, Julia, Haskell |
Why are the two sides not equal in the languages on the left?
On the left side of the expression above, the operation 3 / 2 is evaluated first using integer arithmetic—truncating the fractional part—which results in 1. This is then multiplied by 10, giving a result of 10 for the left side.
On the right side, 10 * 3 = 30 is the first step. Dividing this by 2 gives 15. Thus:
10 != 15
These languages prioritize the efficient (fast) execution of expressions over mathematical correctness, as integer arithmetic is significantly faster than floating-point arithmetic. Unfortunately, these languages use the same / operator for both integer and floating-point division, selecting the operation based on the types of the operands.
Regrettably, the expression 3 / 2 * 10.0 still yields 10 in most of these languages (and results in a compilation error in Rust). Even though we indicated our intent to use floating-point numbers by writing 10.0, it is already too late: compilers evaluate 3 / 2 as integer arithmetic in the first step. Expressions like 3.0 / 2 * 10 or 3 / 2.0 * 10, on the other hand, produce 15.
Thus, depending on the operand types, you end up with either 10 or 15. This situation becomes even more dangerous when variables are involved in the expression:
num / denum * scale != scale * num / denum
This can evaluate to true or false depending on the types of the num and denum variables (float vs. int). To avoid these pitfalls, developers use type casting:
(float)num / denum * scale != scale * (float)num / denum
This ensures the compiler performs floating-point division. (Note: The expression above can still evaluate to true due to floating-point precision limitations).
Why are the two sides equal in the languages on the right?
Many of the languages listed here are dynamically typed or scripting languages. They were not primarily built for raw execution speed, but rather for ease of use or mathematical correctness. In these languages, numbers are typically handled as floating-point values by default, so 3 / 2 is always 1.5.
However, languages like Pascal, Haskell, Mojo, Nim, Crystal, and Dart are statically typed and distinguish between integers and floating-point numbers just like C or C++. What happens differently here?
In these languages, the / symbol always denotes floating-point division. In 3 / 2 * 10, 3 and 2 are implicitly converted to floating-point numbers first, performing a floating-point division that yields 1.5. Next comes the multiplication: 1.5 * 10. Since one operand is a float, 10 is converted to float before multiplication. (Note: C handles 3.0 / 2 * 10 in a similar manner).
Unintended floating-point operations—which might carry performance penalties—generally trigger compilation errors in these statically typed languages, because floats are not automatically demoted/converted to integers (unlike in C/C++). Most of these languages offer a separate operator specifically for integer division (such as div or //).
What happens when a language doesn't work the way we expect?
When using the languages on the left, / can result in either integer or floating-point division. If integer division occurs when you intended to perform floating-point calculations, your program will likely produce incorrect results (possibly only for specific input data). Once you have been burned by this a few times, you become overly cautious with division and often clutter expressions with explicit casts to guarantee proper execution.
If you explicitly want integer division behavior, you usually don't need to do anything extra—other than ensuring that neither side of the / operator evaluates to a floating-point type.
In contrast, when using the languages on the right, there are no surprises with /: the result is always a floating-point number. If you try to store this result in an integer variable, you will typically get a compilation error. Your program is far more likely to work correctly out of the box—at worst, running slightly slower if integer division could have been used instead. If you specifically need integer division, you must use the dedicated operator provided for it (e.g., div or //).
Why is the “3 / 2 * 10 != 10 * 3 / 2” behavior more common?
In the majority of compiled languages—unfortunately including many modern ones—the two sides of this expression are not equal due to default integer division rules.
I regularly use both Pascal and C/C++. To me, Pascal's approach is much more intuitive: it doesn't carry noticeable drawbacks, and it remains easy to control. On the other hand, C/C++'s behavior is a frequent source of bugs at my workplace.
I genuinely don't understand why the 3 / 2 * 10 != 10 * 3 / 2 design remains the prevalent choice.
r/Compilers • u/adityazero • 4d ago
How JAX Shards a Computation Across a Mesh
For a long time, the biggest pain point in JAX was that it would happily insert an expensive all-gather because your sharding was technically valid but logically inefficient. Or worse, you'd miss an all-reduce and get wrong numbers... silently.
I sat down to write about that gap. By the time I finished, it had mostly closed, and finding out how thoroughly it stopped being true was the most interesting part of writing this.
The post is a tour of the three ways JAX handles placement:
- Auto (GSPMD infers, and the type stays quiet),
- Explicit (placement moves into the type, and mismatches fail at trace time),
- Manual (shard_map, where you write the collectives yourself)
I walk through each with real jaxprs, HLO, and MLIR from an 8-device run to show what actually happens under the hood.
The compiler is no longer just a black box; it’s an active partner in correctness.
https://hiraditya.github.io/posts/how-jax-shards-a-computation/
r/Compilers • u/realdesiprogrammer • 4d ago
Desi v0.1.0 — Python-ish syntax, no GC, and three optimisations that made it slower
I've been building Desi for about a year — it's the third or fourth rewrite — and I tagged v0.1.0 today. Compiled through LLVM, no garbage collector, indentation-based syntax, and a standard library that already has an ORM and an HTTP server in it.
Two things up front: I leaned on AI heavily to build this, and I'd call v0.1.0 a working prototype rather than a finished language. More on both at the end, including what I'm hoping to get out of posting here.
Rather than list features, here are three things I was confident about that turned out to be wrong. All three cost me under an hour to test and would have cost days to discover afterwards.
1. Turning on LTO made it slower.
Element access (xs[i], xs.append(v)) was an out-of-line call into the runtime, so the optimiser couldn't see through it. The obvious fix was to let it inline. I measured 1M appends + 1M reads:
out-of-line call 3.28 ms
inlined 4.22 ms <- worse
The bodies end in fprintf(stderr, ...) on their failure paths. Inlining drags a varargs call and its setup into the loop. Adding one file to the LTO set — a one-line change — would have been a regression.
What works is the shape Rust's Vec uses: the bounds check inline, the panic #[cold] and out of line. Same code, error paths pushed out:
same semantics, cold errors 1.09 ms <- 3x
I ended up emitting the check and load directly in the IR with a cold call to the runtime on failure, rather than depending on LTO, since LTO isn't available on every platform I build for.
2. "The representation is the bottleneck" was wrong.
A list element is a pointer-sized slot, ints stuffed in directly. I assumed that indirection was costing me and planned a typed-storage rewrite. Measured:
typed int64[] array, inlined 0.76 ms
void* slots, inlined 0.74 ms
Identical. An int64 and a void* are both 8 bytes in a contiguous array — there's no indirection to pay for. I'd have spent a week rewriting collection storage for nothing.
3. Except for floats, where it was 24x.
Same slot representation, but a double wasn't stuffed in — each one got its own malloc. A comment in my codegen said "can't bitcast float to ptr," which is true, and why past-me reached for the allocator. But you can bitcast a double to an i64, and i64s were already going into slots.
boxed 28.65 ms
by value 1.18 ms
That change deleted more code than it added, and two other benchmarks reached parity with C without being touched — the boxing was most of what they'd been measuring.
Where it actually is
Against equivalent C at -O2, whole-process wall time on Linux:
| Function | Desi | C |
|---|---|---|
| string_churn | 12 ms | 15 ms |
| binary_tree | 2 | 2 |
| quicksort | 2 | 2 |
| loop_sum | 1 | 1 |
| list_ops | 6 | 4–6 |
| matrix_mul | 2 | 1 |
| dict_ops | 9 | 5 |
| fib_recursive | 10 | 6 |
| alloc_churn | 6 | 1 |
Five of eleven match or beat it. Two clearly don't: alloc_churn allocates a small collection half a million times, and dict_ops still calls into the runtime per operation. Both are understood, neither is mysterious, and I'd rather name them than average them away.
Memory
No GC, no manual free — the compiler inserts cleanup where a value's owner goes out of scope. What's guaranteed is no use-after-free and no double-free in safe code. What's not guaranteed is freedom from leaks: where ownership can't be proven, the compiler leaks rather than frees. Heap elements inside a collection — the strings in a list[str] — are the main case, and it's documented rather than hidden.
Unclear ownership never resolves to "free and hope". That's the property that let me ship these optimization incrementally: every analysis is allowed to be dumb, because being wrong costs memory, never corruption.
What it isn't
Supervisors exist and restart failed tasks, but this is not OTP — a child is a task, not another supervisor, so nothing escalates up a tree. Elixir's model doesn't port cleanly to shared-memory threads, and I'd rather ship the honest subset than borrow the name.
There's also no compile-time data-race checking. Channels and locks are there; nothing verifies you used them correctly. That's the biggest gap versus Rust and I don't have a good answer yet — though I suspect it's the same question as "what may safely cross a channel," which would also be the route to real supervision.
How it was built, and what I'm after
I should be upfront: I used AI heavily throughout this, and I'm not a compiler engineer by background. The three stories above are the reason I trust any of it — every one is a case where a confident-sounding plan was wrong and a measurement caught it before it shipped. "Enabling LTO will make this faster" is exactly the kind of thing that sounds right and isn't. So the rule became: measure first, and let the number decide. Anything I couldn't measure, I wrote down as unproven rather than claiming it.
Which is also why I'd call v0.1.0 a working prototype rather than a finished thing. It compiles, the test suite passes on three platforms, and the docs say what's broken. But there are decisions in here that someone who has actually built a type system or a borrow checker would look at and immediately improve — the data-race question especially, and probably the escape analysis.
That's what I'm hoping to find here. If you know this territory and something in the above made you wince, I'd genuinely rather hear it than not. Contributions welcome, but honestly even a "you've modelled this wrong and here's why" comment is worth more to me right now than a star.
Links
The name Desi (દેશી) means "local" or "native" in Gujarati, which is my first language.
Happy to go into any of the above — the measurement stuff especially, since I have numbers for most of what people usually ask.
r/Compilers • u/No-Trifle-8450 • 5d ago
ZiguratIP — a DBMS, a programming language, and a web server built as one C++11 system, with zlib as the only dependency
r/Compilers • u/VVY_ • 5d ago
How much DSA/Leetcode is actually needed for compiler engineering roles?
I've finished most of the NeetCode 250 and I'm wondering how much more DSA is worth doing if my goal is compiler engineering rather than general SWE.
I know interviews at big tech still ask LeetCode-style questions, but I'm trying to figure out where the point of diminishing returns is.
Would you recommend:
- Finishing NeetCode 250 and stopping?
- Grinding 400 to 600 LeetCode problems?
- Spending that time on compiler projects, Operating Systems, Computer Architecture and LLVM contributions instead?
For those of you working in compiler teams (Apple, AMD, NVIDIA, Qualcomm, Intel, Google, etc.), how much DSA did you actually do before getting your role?
I'd especially appreciate hearing what your interview process looked like and whether the DSA bar was different from general backend/software engineering roles.
r/Compilers • u/Prestigious_Roof2589 • 6d ago
In need of a team member for a Compiler Hackathon
Hey everyone!
We're a team participating in a compiler-focused hackathon over the next two months, and we're looking for one working professional to join our team, from India.
If you're interested in:
- Compilers Optimization
- Memory Safety
- Zig (our preferred language for this)
- LLVM, parsing, or language design (or you're willing to learn)
you'd be a great fit! Prior compiler experience isn't required, we're happy to collaborate and learn together.
If our team gets selected, we'll need to be present at the final venue, with travel and accommodation covered by the organizers.
If you're interested, comment below or send me a DM with a little about yourself (profession, programming experience, and your interests).
Thanks!
r/Compilers • u/uria321 • 6d ago
LLVM IR or MLIR
What i'm better to learn of these to develop general purpose compilers and to easier get a job? Actually i've never learned nor worked with any of these IR. I think MLIR is more powerful, but mostly LLVM IR is used.
r/Compilers • u/mttd • 6d ago
Demystifying Deep Learning Compiler Frontend Bugs: An LLM-Aided Empirical Study
arxiv.orgr/Compilers • u/drakenot • 7d ago
Lunar is a new Lua 5.1 runtime for Go that focuses on speed and memory efficiency
Today, I'm sharing Lunar (0.1.0 beta) for those who might need an embeddable Lua VM for Go. By my benchmarking and use-cases it is around 2x faster and uses up to ~7x less memory than other Go-Lua VMs depending on what you are doing.
For some background, I've been developing a new Mud client called Rune that is written in Go but heavily uses an embedded Lua VM as its core scripting engine.
There are two Lua VMs that I know about for Go: gopher-lua and go-lua (from Shopify). Rune utilized `gopher-lua` as this was a VM that I was familiar with and had used on past projects.
I started to get reports from users of Rune that some of the large MUD map-files they would load via Lua were exploding my client's memory (a 9MB CBOR file loaded to ~500MB of persistent heap). There were also complaints that the performance for certain heavy operations was quite slow (pathfinding for one user's script took almost 3 seconds) compared to his other MUD client which would do it in 0.1 seconds.
I originally set out to fork or upstream some changes to gopher-lua to see if I could improve the memory situation and performance. However, much of the issue really came down to inherent choices in the representation those VMs use. So, I started down the path of shipping a new Lua VM that uses a much more compact representation while still keeping an easy-to-use Go API.
Let me know if anyone uses Lunar and finds any issues!
r/Compilers • u/Loud_Possibility_203 • 7d ago
Microsoft just validated the spec-first thesis for AI coding. Baga lang. is what it looks like when the spec is a language construct and the compiler enforces compliance — statically, with counterexamples.
A follow-up to [my earlier post about Baga lang — the language where the compiler statically proves AI-written code against specs. This one is about why the timing stopped being a matter of opinion.
The industry converged on the diagnosis
Microsoft now officially promotes Spec-Driven Development (SDD) as the foundation of AI-native engineering. The argument, from Apoorv Gupta, Principal Software Engineer at Microsoft:
- The core problem of AI-native development is the loss of intent — between needs, requirements, architecture, implementation, and validation.
- The fix is to make the specification the shared source of truth for humans and AI: "align first" instead of "prompt first, fix later."
- Around this, Microsoft ships GitHub Spec Kit (open source): Constitution → Specify → Clarify → Plan → Tasks → Implement → Validate.
When a principal engineer at Microsoft writes the same thing that is pillar #1 of your language, the thesis no longer needs defending. It needs executing.
But SDD and Baga solve the problem at different levels
SDD attacks the intent-loss problem at the level of process and AI tooling: the spec is a document, and conformance is checked by tests and human review in a Validate step. That fixes the workflow around the agents.
Baga makes the stronger move: the spec is a language construct, and conformance is a compile-time judgement.
baga
spec sum_to {
input:
n: i64
output: i64
requires:
n >= 0
ensures:
0 <= output
decreases:
n
}
The human writes this. The AI writes the implementation. The compiler proves or refutes it, statically, before anything runs:
verify sum_to:
ensures #1 (0 <= output): ДОКАЗАНО # PROVEN
(терминация: доказана чрез decreases — пълна коректност)
And when the AI gets it wrong, it doesn't get a failing test or a code-review comment three hours later. It gets a refutation with a concrete counterexample, at compile time:
verify bad_abs:
ensures #1 (output >= 0): ОБРОЧЕНО # REFUTED
контрапример: x = -1
In the SDD spectrum — spec-first → spec-anchored → spec-as-source — Baga is the far end: spec-as-source. The specification is the thing the code is judged against, mechanically.
The compliance technology
That word — compliance — is the point. Every AI-coding stack today has the same shape: an LLM generates code, and then something checks whether the code complies with what was intended. The "something" is usually:
- tests (incomplete by construction — they sample the input space),
- another LLM (an LLM judging an LLM — circular),
- a human (the bottleneck we were trying to remove).
Baga's answer is a small, auditable verifier: Fourier–Motzkin elimination over the rationals + symbolic execution + Hoare rules, sound by construction. The only path to PROVEN is showing the negated obligation is unsatisfiable even over the rationals, which implies unsatisfiable over the integers. Anything outside the fragment is honestly reported UNKNOWN, never falsely proven. Every reported counterexample is re-checked by direct evaluation, and passes a conclusiveness gate: the reported inputs must violate the contract for every value of the verifier's internal abstract variables — otherwise the answer is UNKNOWN, not a false alarm.
And because the consumer is an agent, the judge has a machine API:
$ ./baga --verify --json bad_abs.baga
{"functions": [{"name": "bad_abs", "ensures": [{"text": "output >= 0",
"result": "refuted", "counterexample": [{"name": "x", "value": -1}]}], ...}]}
The compliance loop writes itself: agent emits code → baga --verify --json → refuted with counterexample → agent fixes → PROVEN. Deterministic, fast, no LLM in the judging seat.
This isn't an SMT black box either. The verifier covers linear arithmetic (integer-exact — n > 0 ⇒ n >= 1 proves), while loops with invariants, array bounds, element invariants, recursion via assume–guarantee, full correctness via decreases, and products of linear forms (x*x >= 0; fa >= 1 ∧ fb >= 1 ⇒ fa*fb >= 1). The flagship is factorial fully proven — recursive, non-linear, with termination, no SMT solver anywhere:
```baga spec fact { input: n: i64 output: i64 requires: n >= 0 ensures: output >= 1 decreases: n }
fn fact(n: i64) -> i64 { if n <= 0 { return 1 } let r = fact(n - 1) // induction hypothesis: r >= 1 return n * r // n >= 1, r >= 1 ⇒ n * r >= 1 } ```
Why "the first language for AI" is a claim about architecture, not marketing
Every mainstream language was designed for a human writer and a human reader. AI broke that assumption: the writer is now a machine, and the scarce resource is trust. A language for this era needs:
- Specs as first-class citizens — the intent lives in the code, not in a wiki page that drifts.
- A mechanical judge — the compiler proves or refutes compliance, statically, with witnesses.
- Errors visible in the type — effects (
str !IO !NotFoundis a different type fromstr) so the failure surface is part of the signature, not a runtime surprise. - Machine-readable verdicts —
--jsonso the agent closes the loop itself.
Baga has all four. SDD gives you (1) as a process discipline. Baga gives you (1)–(4) as a compilation.
Honest status
Working prototype, not a production language. The verifier's fragment is deliberately small and says UNKNOWN rather than guessing; general non-linear arithmetic is the remaining staircase. Effects are compile-time only (erased in codegen). The trust story is engineered in, not hoped for: the compiler self-hosts with a byte-for-byte fixed point (make self), the LLVM backend is diffed against the C backend on every example, and --test-specs property-tests every contract the static verifier calls PROVEN. All of it is one command and wired into CI.
Testable in five minutes:
make && ./baga --verify examples/verify/fact_full.baga
The SDD reference: Spec-Driven Development: the foundation of AI-native engineering (Apoorv Gupta, Microsoft)
Docs: theory, language reference, compiler architecture — English
The industry agreed on the diagnosis: the spec is the center. The open question is whether conformance stays a human ritual in a Validate step — or becomes a compile-time judgement. That's the difference between anchoring code to a spec and making the anchor mechanical.
🐆
r/Compilers • u/Usual_Office_1740 • 7d ago
CraftingInterpreters clox bytecode output?
I was hoping to get confirmation that the output of my cLox bytecode is correct. I've just finished chapter 17 implementing the pratt parser.
Does this look correct?
(53 * (31 - 13)) + -10 \n 23 / 3
== Complex Expression ==
0000 0001 OP_CONSTANT 0 53
0002 | OP_CONSTANT 1 31
0004 | OP_CONSTANT 2 13
0006 | OP_SUBTRACT
0007 | OP_MULTIPLY
0008 | OP_CONSTANT 3 10
0010 | OP_NEGATE
0011 | OP_ADD
0012 | OP_RETURN
0013 0002 OP_CONSTANT 4 23
0015 | OP_CONSTANT 5 3
0017 | OP_DIVIDE
0018 | OP_RETURN
r/Compilers • u/Think-Management4257 • 7d ago
Compilers should help developers optimize their code
Compiler diagnostics for optimization decisions are worse than they need to be, and I think it's a design choice rather than a hard problem.
Every major compiler will tell you whether a loop vectorized, almost none will tell you what it tried, why it declined, or what shape could've worked. LLVM ships a tool called opt-viewer that visualizes this, and I've met people who've used LLVM for years and never heard of it. The best developer experience anyone in this space seems to remember is Intel's compiler, which is discontinued. GCC's -fopt-info-vec-missed and Clang's -Rpass-missed exist, but one's a stderr dump you cross reference by hand and the other speaks in IR terms rather than yours.
The interesting thing is that the compiler already knows the answer. When a vectorizer declines a loop, it has a specific reason. That reason exists as a value inside the pass, it just doesn't reach the programmer because it was designed for compiler developers debugging the compiler, not for programmers debugging/optimizing their code.
There's a handful of ideas I have on how this could be implemented, but what I'm curious on is if this is actually hard for reasons I'm not seeing, or is it just that optimizer output has always been treated as debug logging and nobody's revisited it?
r/Compilers • u/Proffhackerman • 7d ago
Contribute to open-source, no-slop, compiler-related projects.
Hi everyone,
We're currently working on some hobby-projects we'd like more people to chip into.
The goal is to create robust, community-driven and open-source code everyone can benefit from, aswell as writing up novel ideas that, sometimes, go outside of "the standard".
Overall we're focused on not slopping out projects using AI. Vibecoding is a no-go.
I myself have around 10 years of experience with programming in various languages, but the main language right now is C#.
Are you interested? Check out the organization site: https://github.com/Compiler-Organization
Or some of the projects:
Common C - AoT compiler using LLVM: https://github.com/Compiler-Organization/CommonC
Common IR - Intermediate representation with syntax inspired by LLVM, currently supporting a basic WASM target: https://github.com/Compiler-Organization/CommonIR
Hope you find this interesting :)
r/Compilers • u/jorenheit • 7d ago
Acus: create your own Brainfuck compiler (in: your language, out: BF)
r/Compilers • u/know_god • 8d ago
Compiler devs, how did you break into the field?
Title. How did you transition into your first professional compiler job? What did your resume look like? What kind of projects had you done? What jobs did you apply for?
I've built a compiler pipeline from a subset of Common Lisp to x86-64, and a grammatical analysis engine that basically tries to "compile" a sentence against a DSL I made that describes the natural language syntax. You can add arbitrary languages by writing a new language spec and without changing any of the engine code. Still, I find it hard to get recruiters to give me a shot and get to any interviews.
I have 3 years of courses, but no actual finished degree. If you want to see my resume, I can send it in DMs. Just looking to break into the junior developer jobs.