iiinova — where your digital self keeps evolving

Yeah definitely, though even with formal proofs it’s very easy to prove strong theorems with impossible preconditions. It remains key to show you can admit real instances of the theorem.

040

xav @xavxav.bsky.social · 04/09/2026

Every formal verification practitioner also knows Knuth’s “Beware of bugs in the above code; I have only proved it correct, not tried it.”, and yet

1122

xav @xavxav.bsky.social · 31/08/2026

La gestion rigide et très hiérarchique à la française y sont pour beaucoup de ce qu’on m’a raconté

140

xav @xavxav.bsky.social · 31/08/2026

Il y a aussi la question de l’émigration, toutes les grandes boîtes américaines on des colonies d’ingénieurs français. Et ce n’est pas seulement du à la différence de salaires de ce que j’ai entendu.

131

Reposted by xav

SE Gyges @segyges.bsky.social · 27/08/2026

i propose a moratorium on doing things that seem sinister

0432

Reposted by xav

Stephen Jacob Smith @stephenjacobsmith.com · 24/08/2026

Disappointingly superficial. New York City has huge issues building anything underground, and the coordination issues mentioned in passing here are a huge reason why. But all the most well resourced newspaper on earth can muster about its home city is "the street markings look like abstract art"?

nytimes.com

Behind the Mysterious Symbols Spray-Painted on Our Streets (Gift Article)

All over New York’s sidewalks and sewers, colored markings hide in plain sight, telling construction crews where to dig and creating accidental art.

61008

xav @xavxav.bsky.social · 16/08/2026

bsky.app/profile/kohn...

000

xav @xavxav.bsky.social · 22/07/2026

Haha I added a `#[boxed]` macro for that entire reason.

030

xav @xavxav.bsky.social · 22/07/2026

true, though I wouldn’t be surprised if llvm had an n^3 hiding somewhere.

110

xav @xavxav.bsky.social · 22/07/2026

True but look at the pass timings of a non trivial rust project, type checking / borrow checking is usually a quite small part (<10% at work) of compile time.

140

Reposted by xav

rev. howard arson @theophite.bsky.social · 03/03/2025

quitting my tech job to make pig iron in a crucible in my backyard

1330317

xav @xavxav.bsky.social · 29/06/2026

It seems unlikely that it’s valid to me because the major clouds would otherwise have a _massive_ interest in breaking up a putative cartel. It seems more likely these clouds draining all supply and it takes (many) years to build new fabs

000

Reposted by xav

Cyrus Omar on sabbatical in Cambridge @neurocy.bsky.social · 17/06/2026

Really nice work by Celeste Barnaby and colleagues at #PLDI on active learning for program synthesis. Various synthesizers, including LLMs, can produce multiple candidate programs given an underspecified intent. This system figures out multiple choice questions to ask the user to disambiguate.

Slide screenshot. Title: "Choose, Don't Label: Multiple Choice Query Synthesis for Program Disambiguation". What is this paper about? A. An active learning framework using multiple choice queries. B. An approach for synthesizing informative and interpretable queries. C. A new tool called Socrates that improves accuracy and usability. D. All of the above (checked). QR code to Try Socrates

151

Reposted by xav

rain 🌦️ @sunshowers.io · 16/06/2026

Soteria actually works on a complex Rust project!

141

xav @xavxav.bsky.social · 16/06/2026

The specific tech inside soteria is novel and generally more extensible. Soteria instantiates it in a way that lets it reason natively in rust semantics rather than compiling through a c proxy like a lot other tools. This gives a _real_ speed up

030

xav @xavxav.bsky.social · 16/06/2026

Does anyone have a good solution for cargo caching in ci? With large (10gb+) amounts of target/ data to cache

020

xav @xavxav.bsky.social · 12/06/2026

Yeah Sacha is well aware of the challenges of ocaml, and I think agrees with you on its problems.

110

xav @xavxav.bsky.social · 12/06/2026

My PhD thesis felt like a constant struggle with the ocaml community, despite my best efforts to keep it at arms length it’s jank kept sneaking back into my work. The idea that you should be able to just download and run a program is so alien

010

Reposted by xav

opale !! @n1ark.acouphene.net · 10/06/2026

self promo we did a blog post to launch the startup thing we're working on ^-^ i do the rust stuff it's cool you should try it out if you like unsafe rust ill probably do a blog post on some fun performance work i did on tree borrows #soon! soteria-tools.com/blog/introdu...

soteria-tools.com

Introducing Soteria: A New Generation of Static Analysis for Rust - Soteria

Find bugs today. Teach AI to find them tomorrow.

2338

xav @xavxav.bsky.social · 09/06/2026

Very cool! I’ve long wanted to build a “PL IDE” along the lines of what you discuss in your post, where you co-evolve dyn/static semantics, using models to synthesize candidate programs/rules and example based feedback to refine them

010

xav @xavxav.bsky.social · 25/05/2026

I want to improve it to give me the cost of each _line_ not just each source function.

020

xav @xavxav.bsky.social · 25/05/2026

picked this back up and turned it into a tool that can estimate within 10% the compile cost of functions. Think of it like cargo llvm-lines that rolls up to functions in your crate

142

xav @xavxav.bsky.social · 25/05/2026

Have you seen ho native_compute works in rocq?

220

Reposted by xav

Doll @dollspace.gay · 24/05/2026

The problem with bluesky is that it’s not written in rust

4442

xav @xavxav.bsky.social · 22/05/2026

At work we have a k8s controller, first thing I did was full rust rewrite. Zero regrets

010

xav @xavxav.bsky.social · 21/05/2026

i've been enjoying my time using jj, but i have to say, i've never 'lost' so much work since starting with jj. the anonymous commits, optional descriptions and lack of locally tracking bookmarks means i end up with tons of "temporary" commits lost on my tree i can never find again.

000

xav @xavxav.bsky.social · 19/05/2026

That’s basically the inspiration, via megaparsec in Haskell

000

xav @xavxav.bsky.social · 18/05/2026

Yeah we do control both but we want a specific serialized repr, which interferes with the open api form.

000

xav @xavxav.bsky.social · 18/05/2026

Doesn’t help that we use untagged because we want our json interface to be ergonomic / have opinions on it.

100

xav @xavxav.bsky.social · 18/05/2026

Ah yeah but that’s what I meant by pattern matching, your code generator has to be aware of that trick and able to leverage it to generate nice types.

220

xav @xavxav.bsky.social · 18/05/2026

Isn’t oneof untagged?

100

xav @xavxav.bsky.social · 18/05/2026

But you’re sort of working around open api there no? Since all you have is oneOf? I’m sure there are ways you can pattern match certain forms to generate nice enums, but we found ourselves with a lot of any types for our filters in basically every language. Maybe that’s more of a stainless problem

100

xav @xavxav.bsky.social · 18/05/2026

I hate how open api is so hostile to sum types, it really wants everything to be bags-of-objects. There’s no good way to get it to express a lot of common rust types.

160

xav @xavxav.bsky.social · 17/05/2026

I’m NL for RustWeek, come see my talk! If you want to chat send me a message :)

050

xav @xavxav.bsky.social · 16/05/2026

isn’t the value of these shares the ownership they represent? If they’re stripped of all power what do they actually own?

010

Reposted by xav

Quantian @quantian.bsky.social · 14/05/2026

The board consists of three semi-literate car dealers who were the state’s top GOP donors. Their top priority is fighting wokeness in the Potato School by putting up a statue of the confederate general who owned the largest potato farm in the state in 1859.

122304181

xav @xavxav.bsky.social · 07/05/2026

That doesn’t really capture what I want: often I’m keeping a benchmark or test unstaged and bouncing between trunk & branch to diff. I don’t want a merged view of everything.

100

xav @xavxav.bsky.social · 07/05/2026

it’s weirdly the part I struggle with the most, I used unstaged changes to keep things while I bounce between different branches.

130