CS researcher. Scala 3 Compiler Lead @EPFL. Scala Core Team & SIP Committee. Agonizing over types, effects, tracked capabilities, separation & freshness.
Switzerland
Joined June 2016
- Tweets245
- Following126
- Followers320
- Likes596
Pinned Tweet
We've released ATC, a new open-source coding agent based on Tacit. It uses tracked capabilities to control what agents can do, and works with Claude and Codex subscriptions as well as API providers.
Funded by the Swiss Cyber-Defence Campus. Enjoy!
github.com/lampepfl/atc
When Carmack says “functions that return with the stack extended,” that’s precisely what we did in “What If We Don’t Pop the Stack?” (ECOOP’22).
Return a stack-allocated value → leave the frame. Reclaim only when a 1st-class value comes back. 10–25% faster in our benchmarks from less heap traffic + better locality.
drops.dagstuhl.de/entities/d…
I always thought it was a shame that modest default stack setups made alloca() a generally-frowned-upon technique in C/C++. With 64 bit architectures, give every stack a virtual address space equal to the physical memory by default!
You can do a surprisingly good job of memory management with just the stack, and I contend that it has both correctness and performance advantages.
Allocations are a trivial pointer adjustment, and frees are literally free. Keeping everything linearly packed is friendlier for all layers of the cache hierarchy, and it makes keeping everything in huge / gigantic pages easy.
Leaving temporary intermediate blocks on the stack can seem wasteful, but unless you are dealing with algorithms that make > O(n) temporary allocations, it is usually not a big deal.
Static analysis can check if you store a stack pointer into a structure deeper in the stack, which is a use-after-free, and then memory management correctness is guaranteed.
The discipline of caller-allocates-return is awkward in some dynamic cases. It would take a change in low level calling conventions, but you could plausibly have functions that return with the stack extended from where it was when they were called. I’m not holding my breath for that.
It isn’t obvious if having AI coding agents makes discussions of software architecture more or less important!
I’d argue Scala 3 and OxCaml are spearheading some of the most exciting developments in programming languages. Unfortunately they’re overshadowed by all the AI hype. But that’s temporary: their relevance to AI-generated code is already becoming clear and will only grow.
Oliver Bračevac retweeted
I'm happy to share that Mojo and MAX are now fully open - for development, extension, and commercial use! This includes the full Mojo programming language, but also the MAX graph compiler, MLRT runtime internals, and hardware abstraction logic.
Get your agents going!👇
Oliver Bračevac retweeted
Historical moment indeed: formal methods are now verifying real-world binaries at scale! But the specs are single-entry (not API), proofs are huge, and reuse is largely copy-and-adapt. Compositional reasoning and modular abstractions are how the FM community can make this scale.
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
I’m surprised how many in the Scala community still conflate library-defined effect systems with tracking the effects of the language itself.
Tracking effects in a library-defined computation is not the same as tracking the effects of the programming language itself. 1/5
And this is becoming even more relevant with LLM-generated code. Do we really want to rely on coding agents respecting library conventions?
I find it strange that we’re making progress on these problems in Scala 3, while much of the community seems unaware of it. 4/5
Sure. TACIT already works with OpenCode via MCP & its native tools disabled. ATC gives us a setup to experiment with capability-aware execution and permissions, but adapting an existing harness is possible. The important bit is that its tools cannot bypass TACIT.
Yes! That could be a good fit. ATC checks capabilities while Sandcat adds process and network isolation. We're currently looking into sandboxing for the next project phase, particularly how the capabilities we track can inform the sandbox policy.
😱 !
Would it make sense, that #sandcat from @VirtusLab adds support for atc ?
Hence, proxying in a safe way Claude ?
Yes! ATC is the agent harness, and not merely a wrapper around model API calls. More precisely, it disables or avoids the providers' native local tools and supplies its own capability-controlled execution path.
Oliver Bračevac retweeted
The End of Programming? Video of my talk yesterday at #scaladays. youtube.com/watch?v=jlJyuJhD…
As younger generations grow up surrounded by LLMs, they may internalize “LLM speak”so thoroughly that AI-text detection becomes meaningless. Imagine Anthropic’s watermarks surviving not just in generated text, but in actual meat brains.
Oliver Bračevac retweeted
New Scala LTS is out! Read all about it in the recent blog post by Wojciech Mazur at scala-lang.org/news/3.9/. The blog post covers all the most recent features, a quick reminder of all the ones since the last LTS, and practical information about migrating.
