Tessera
Folgen

Max

@bernsteinbear.com

Baking bread and compilers are kinda similar if you think about it @tekknolagi elsewhere bernsteinbear.com

457 Posts442 Follower85 Folgt
Max@bernsteinbear.com · 5d ago

Have you all ever had a Google workspace Group ever silently drop emails to its members? I just discovered that we're missing emails left and right. They appear in the log on the admin console but not in our inboxes or spam.

Max@bernsteinbear.com · 6d ago

All that effort to implement sparse conditional constant propagation only to find out that fixpoint looping over RPO is faster

Max@bernsteinbear.com · last wk.

I love getting push notifications that Sofi Tukker dropped a new song. Probably the only kind of unsolicited notification I appreciate

Max@bernsteinbear.com · 2w ago

So the cool thing about hotel room locks being battery powered is that the batteries die and you can't get into your room. Isn't that fun?

Max@bernsteinbear.com · 2mo ago

If I had a nickel for every programming language implementation funded by ill-gotten World of Warcraft hacking gains, I'd have 1. Which isn't a lot, but it's still surprising

Philip Zucker@sandmouth.bsky.social · 2mo ago

On Monday morn I'll be giving a talk at @sigplan-pldi.bsky.social #PLDI EGRAPHS 2026 about lifting egraphs pldi26.sigplan.org/details/egra... a new twist on adding a notion of rigid alpha canonical variables to e-graphs! Pretty pumped about these ideas! Check it out!

Lifting E-Graphs: A Function Isn’t a Constant (EGRAPHS 2026) - PLDI 2026

Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via eq...

pldi26.sigplan.org

Max@bernsteinbear.com · 2mo ago

Incredibly fortunate to have noticed that a Joe's pizza opened in my neighborhood, gone in, gotten a slice, and learned that it opened today!!! Life is good

Aaron Patterson@tenderlove.dev · 2mo ago

Probably silly but I'm really proud of this PR. It was challenging, fun to work on, and I think it'll have a big impact long term. 🤞 github.com/ruby/ruby/pu...

Reserve 2 bits for expressing object layout by tenderlove · Pull Request #17139 · ruby/ruby

We would like to make instance variable reads in the JIT compiler faster (as well as simplify the JIT implementation). Currently, in order to read an instance variable, we have to: Test for heap ...

github.com

Kiran@kirancodes.me · 3mo ago

Z3! You're on WATCH! Latest update to lean.py is a drop in replacement for Z3! Everyone's trying to put SMT solvers in their theorem prover, how about putting a theorem prover in your SMT solver? and here's the crazy thing: One click install, if you know Z3, you KNOW lean.py. You are not ready.

A Z3-like reasoning API for Python, backed by Lean 4 Lean 4 is a general-purpose symbolic reasoning engine. Its tactic library covers linear arithmetic (omega), congruence closure with E-matching (grind), propositional decidability (decide), and rewriting (simp), and the system is designed to be extended with new sorts, constructors, and decision procedures. Every proof is independently checked by a small trusted kernel, so the Python side never needs to trust the automation; it trusts the checker. The overhead of learning Lean’s type theory and build system has kept most of this machinery out of reach for Python programmers. lean_py.z3 wraps Lean’s tactic engine in the z3py API. Propositions are written in the familiar Int, Bool, Function, ForAll vocabulary. Under the hood, each expression compiles to a Lean 4 term, gets dispatched to the tactic engine, and the resulting proof is kernel-checked. uv pip install "lean_py @ git+https://github.com/BasisResearch/lean.py" You need elan so that lean is on your PATH. Then open Python. from lean_py.z3 import * x, y = Ints('x y') prove(Implies(And(x > 0, y > 0), x + y > 0)) # proved On the first run the library builds and caches a managed Lake project under ~/.lean_py/managed/, which takes a minute or two. Every subsequent run picks up the cache and starts instantly.
Kiran@kirancodes.me · 3mo ago

ML researchers know Python. Proof engineers know Lean. Never the two should meet.. Until now! Announcing Lean.py, effortless Lean to Python and Python to Lean bindings! - Write Lean tactics in Python - Access the Python ecosystem in Lean github.com/kiranandcode...

Stefan Marr@stefan-marr.de · 3mo ago

The program of ICOOOLPS is now online: 2026.ecoop.org/home/ICOOOLP... And today is the last day for early registrations. Interested in programming language implementation, compilation, and optimization? Join us in Brussels! Don't know what to expect? 1/2

ICOOOLPS 2026 - ECOOP 2026

The ICOOOLPS workshop series brings together researchers and practitioners working in the field of language implementation and optimization. The goal of the workshop is to discuss emerging problems an...

2026.ecoop.org