ngrislain

Thank you, yes, absolutely, and it's also the perfect language for an AI agents. The more refined the type system, the tighter the feedback loop for the agent.

I have been using https://www.passwordstore.org/ for 10 years and am super happy with it. It does not provide all the convenient integrations of 1Password though.

Vibe coding is great. You describe what you want, the agent writes it, the tests pass, you ship. It keeps working right up to the moment it does not: the job gets killed by the OOM reaper in production, or it opens ten thousand file descriptors and falls over, or it runs fine on the sample and melts on the real dataset.

100%, I’ve been writting: Rust, Haskell and Lean 4 with great success with AI. E.g. https://github.com/typednotes/hale

Yes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.

You are right, what I wrote is more of a PoC. It's valid for blocking sockets on the happy path.

Fair point! Updated. I’m definitely coming at this more from a Lean 4/formal methods perspective than a POSIX one.

Just finished

Yes, I'm doing it without AI to learn the language, nonetheless I do think that Lean 4 + AI is a super-powerful combination.

Yes, this year I'm going for Lean 4: https://github.com/ngrislain/lean-adventofcode-2025

It's a great language. It's dependent-types / theorem-proving-oriented type-system combined with AI assistants makes it the language of the future IMO.

A good opportunity to learn a new programming language: https://news.ycombinator.com/item?id=46105849

Advent of Code 2025 in Lean...

Yes it is true that the model has undergone SFT, and RLHF, and other alignment procedures, and hence the logprobs do not reflect the probability of the next token as in the pre-training corpus. Nevertheless, in concrete applications such as our main internal use-case: structured data extraction from pdf documents it revealed very valuable. When the value was obviously well extracted, the logprob was high and when the information was super hard to find or impossible the model would output - or hallucinate - some value with much lower logprob.

We need to build a syntax tree and be able to map each value (number, boolean, string) to a range of character and then to a GPT token (for which OpenAi produces logprobs). This is the reason we use Lark.

Same token usage. Actually OpenAI returns the logprob of each token conditional on the previous ones with the option logprobs=true. This lib simply parses the output json string with `lark` into an AST with value nodes. The value nodes are mapped back to a range of characters in the json string. Then the characters are mapped back to the GPT tokens overlapping the character ranges and the logprobs of the tokens are summed.

Actually, OpenAI provides Pydantic support for structured output (see client.beta.chat.completions.parse in https://platform.openai.com/docs/guides/structured-outputs).

The library is compatible with that but does not use Pydantic further than that.

Haha, I didn't know that one! It's consistent with OpenAI's conception of a "random" dice roll :-D. Joke appart, I'm quite convinced many people would not find 1 or 6 to look "random" enough to be chosen as an example dice roll.

Thank you! Yes indeed, structured output was instrumental in reliably extracting structured data from images from a client.

More precisely it represents the likelihood of seeing this value conditional on the tokens before it.

Thank you! The number is the the sum of the logprobs from the token constituting the individual values. So it does represent the likelihood of seeing this value. So yes OpenAI is super-biased as a random number generator. We sampled other values from OpenAI and got other die roll values, but with much lower probs (5 has 8% chances ).

Imagine you want to open an access to your DB to someone - Alice - you do not particularly trust. And you want to make sure Alice cannot learn anything about an individual in the database.

Maybe you will filter the queries that you assume safe, let's say aggregation queries. But to prevent GROUP BYs with singleton groups, you will enforce some more constraints. Let's says GROUPs should have a minimal size of 10 elements. But then Alice could run a first aggregation with a GROUP of 100 and the same with a GROUP of 100 minus Bob, by using both responses Alice can know things about Bob. Then you will design more involved rules and grow a complex set of rules and eventually add human supervision and your system will not be scalable.

With DP, you add some noise to a query result so that you have a guarantee that nothing substantial can be learned about Bob.

Imagine you want to open your DB to the outside world in a scalable way, you can design a service that: - receives SQL queries - use Qrlew to rewrite them - run the rewritten query on any DB and send back the result as a response - you would also accumulate privacy loss in a privacy accountant so that you make sure the amount of private information leaked by the repeated disclosure of DP query results stays bounded.

That's what Sarus does as a company. Qrlew is the DP-SQL core we use.

I wrote a minimal demo here: https://github.com/Qrlew/docs/blob/main/tutorials/minimal.ip...

There is an interactive playground there as well: https://qrlew.github.io/dp You can change things on the left and then rewritten query shows on the right.

I hope it helps.

Yes Qrlew is based on a research paper (https://arxiv.org/pdf/2401.06273.pdf) presented at a AAAI 2024 workshop: https://ppai-workshop.github.io/

As you may know, Differential Privacy is hard to implement right. To foster trust, we relied on a two-pronged strategy:

- Open-source

- Peer reviewed methodology

Feel free to reach out to us if you need more details.

Qrlew is an open source library written in Rust aimed at bringing Differential Privacy to SQL

nl

You are absolutely right, we are leveraging many open-source bricks to build our product, so that they can be reviewed, mainly:

- https://github.com/google/differential-privacy (for basic mechanisms and PLD accounting)

- https://github.com/tensorflow/privacy (for DP-SGD and RDP accounting)

- https://github.com/opendp (for our SQL module)

We actively contribute to some of them.

We also open-sourced some tech bricks we are using:

- https://github.com/sarus-tech/dp-xgboost (see also https://arxiv.org/pdf/2110.12770.pdf)

We plan to continue building trust in the tools we are using by publishing some of them.

Sarus would typically fit in organizations that legitimately collect personal data and can take decisions based on these data. In these cases you don't want (and most of the time cannot legally) let anyone in the organisation have access to the full personal data records. Using Sarus anyone, even untrusted parties can run analysis on your data safely. These analysis can be classification-model-fitting. You can then classify accurately users to maximize your revenue as long as you can observe the values to feed into your classifier.

At Sarus Technologies, we use dask to test many machine learning models and tune their hyper-parameters in parallel. It's actually quite simple to deploy and scale a dask cluster, thanks to kubernetes and public clouds. If you are interested, check this tutorial out.

Recently, as I was following the 🇺🇸 US elections 🇺🇸, I got puzzled by the fact that days after the elections happened some betting odds of Biden winning the elections were still below 90%, while FiveThirtyEight published a probability of 90% before the election actually happened, when way less information was known.

I decided to spend my Sunday of COVID lockdown illustrating some facts about forecasting, like the martingale property.

A Bayesian perspective on how differential privacy could maintain voter anonymity