Sacha Ayoun

Sacha Ayoun

@giltho.bsky.social

CTO of soteria-tools.com, Scaling Reasoning for the age of AI

67 followers77 following57 posts

Sacha Ayoun reposted

rain 🌦️
@sunshowers.io

The two big projects I work on: * the update system at Oxide. If this breaks, our product cannot be updated any more. The entire update process is autonomous, too * cargo-nextest. ~a quarter of professional Rust devs use it. If this breaks, many people have a bad time So yes, I look at the code

hailey@hailey.at

new poll: do you still even look at the code?

Sacha Ayoun
@giltho.bsky.social

In this new era where I can just make the app I need in an afternoon, Apple is going to have to up its game and let me load my own apps on my iPhone much more easily than whatever the current bullshit is.

Sacha Ayoun reposted

Amos Wenger
@fasterthanli.me

Replying to @fasterthanli.me

I think we should simply stop PL people from naming things until we can figure out what's going on.

Sacha Ayoun
@giltho.bsky.social

You would not believe the crazy stuff this woman has done to make Soteria Rust faster

opale !!@n1ark.acouphene.net

i wrote a blog post about a cool optimisation i did to make quadratic behaviour linear while remaining sound !! its a mix of pretty technical GC details and theoretical Rust stuff, which is the best of mixes imo, go read it !! ! !! soteria-tools.com/blog/meta-ga...

soteria-tools.comMeta Garbage Collection: Using OCaml's GC to GC Rust - SoteriaTracking Rust's aliasing model can be quadratically expensive if done naively. Learn how we fixed this in Soteria Rust by doing meta garbage collection.

Sacha Ayoun reposted

opale !!
@n1ark.acouphene.net

<work> you must be DYING to know how symbolic execution relates to ai ! well wait no more because there was a paper about it and we explain what the paper is about in our latest blog post !! ai !! llms !!! all the stuff people scream about !!! wow ! </work> soteria-tools.com/blog/teachin...

soteria-tools.comTeaching AI to Reason About Software - SoteriaA team at AWS taught a small language model to catch bugs in C by training it on Soteria’s symbolic execution traces, beating a model four times its size. We look at what they did and why it matters.
Sacha Ayoun
@giltho.bsky.social

Let’s gooooooooo

OCaml@ocaml.org

dlvr.itRelease of OCaml 5.5.0We have the pleasure of celebrating the birthday of Blaise Pascal by announcing the release of OCaml version 5.5.0. Release Highlights Some of the highlights of OCaml 5.5.0 are: Module-dependent Functions Modules can now be used as function arguments in a form of lightweight functors. For instance, we can define a function for printing a map generated by the Map.Make functor: let pp_map (module M: Map.S) pp_key pp_v ppf set = if M.is_empty set then Format.fprintf ppf "ø" else let pp_sep ppf () = Format.fprintf ppf ",@ " in let pp_binding ppf (k,v) = Format.fprintf ppf "@[%a@ =@ %a@]" pp_key k pp_v v in Format.fprintf ppf "@[{@ %a@ }@]" (Format.pp_print_seq ~pp_sep pp_binding) (M.to_seq set) We can then apply this function on a string map module String_map = Map.Make(String) with let () = let m = String_map.of_list ["Zero", "Zero"; "One", "Un"] in let pp_str = Format.pp_print_string in Format.printf "%a@." (pp_map (module String_map) pp_str pp_str) m Compared to first-class modules, the type of the function pp_map type 'a printer = Format.formatter -> 'a -> unit val pp_map: (module M: Map.S) -> M.key printer -> 'a printer -> 'a M.t printer is dependent over the value of the module S, and thus the function can only applied over a statically known module: let f (): (module Map.S) = if Random.bool () then (module Map.Make(Int)) else (module Map.Make(Float)) let fail = pp_map (f ()) Error: This expression has type (module M : Map.S) -> (Format.formatter -> M.key -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a M.t -> unit but an expression was expected of type (module Map.S) -> 'b The module M would escape its scope This function is module-dependent. The dependency is preserved when the function is passed a static module argument (module M : S) or (module M). Its argument here is not static, so the type-checker tried instead to change the function type to be non-dependent. Relocatable Compiler A compiler installation can now be moved or copied with no risk of hard-to-debug errors due to mixing incompatible bytecode runtime interpreters. In practice, this means that creating a local switch when there is a global switch with the same compiler version and configuration available can be done by cloning the global switch rather than recompiling the whole compiler. This should considerably reduce the time required to create new local opam switches out-of-the-box. Polymorphic Functions as Function Arguments Higher-rank polymorphic functions can now be defined directly by using an explicit type annotation in a function argument let apply_map (map: 'a 'b. ('a -> 'b) -> 'a list -> 'b list) = map string_of_int [1;2;3], map List.singleton ["x"; "y"] let _ = apply_map List.map Previously defining such a function required going through either a record or an object with a polymorphic field or methods type map = { map: 'a 'b. ('a -> 'b) -> 'a list -> 'b list } let apply_map {map} = map string_of_int [1;2;3], map List.singleton ["x"; "y"] Search and Replace Substring Functions The String module has been extended with many functions for searching and replacing substrings inside a string. let _true = String.includes ~affix:"aba" "abbaba" let sentence = String.replace_all ~sub:"𝄽" ~by:"word" "A 𝄽 is re𝄽ed" The substring search is using the 2-way string matching algorithm which has the advantage of requiring constant space memory overhead independently of the needle size. Generalised Local Definitions It is now always possible to define locally a type, a class, a module type or any kind of item that can be defined globally: let mandelbrot n x = let type t = Converge | Escape of int in ... match orbit n x with | Converge -> 0 | Exit_at n -> colorize n External Types When interfacing with foreign function libraries, it is now possible to define external type type int_gmp = external "mpz_t" type float_gmp = external "mpf_t" Compared to an abstract type definition, the external type name "mpz_t" (resp. mpf_t) makes the type distinguishable from any non-abstract types or external types with a different name. In particular, this makes FFI types better behaved when combined with Generalised Abstract Data Types (GADTs). For instance, The typechecker is able to prove that let ok: (int_gmp,[` A] ) Type.eq -> _ = function _ -> . is a total function because the external type int_gmp is not compatible with a polymorphic variant type. Warning: Abstract types in the current module The astute reader has probably noticed in the definition above that, in OCaml 5.4.0, the typechecker does accept type int_gmp let ok: (int_gmp, [` A] ) Type.eq -> _ = function _ -> . as total. Indeed until OCaml 5.5.0, abstract types defined in the current module type a type b were considered as unique and provably different let f: 'x. (a,b) Type.eq -> 'x = function _ -> . However, this special rule for local definition of abstract types was very brittle. As soon as one moved outside of the current module, it was no longer possible to prove that the types were different. module M = struct type a type b end let fail: 'x. (M.a,M.b) Type.eq -> 'x = function _ -> . Error: This match case could not be refuted. Here is an example of a value that would reach it: Equal This special typechecking rule has been removed in OCaml 5.5.0. If you were relying on it, for instance, because you used an abstract type as type-level label in a GADTs, you can change your abstract type definition to a possibly private abbreviation of a polymorphic variant type a = private [`A] type b = [`B] or a (possibly private) sum type type a = A type b = private B If you were using an abstract type as both a type-level label and a FFI type, you can now use an external type definition which will give you a provably distinct type even outside of the current module. GC improvements Some of the ongoing work to improve the pacing of the garbage collector has been integrated in OCaml 5.5.0, two of the important changes in OCaml 5.5 GC are * the addition of a sweep-only phase at the start of major GC * the addition of an idle phase to smooth the behaviour of the GC at the start. Many incremental changes * The Windows implementation is no more reliant on Winpthreads * Around 60 new standard library functions * Around 90 various improvements * A dozen of documentation updates * Around 40 bug fixes Please report any unexpected behaviours on the OCaml issue tracker and post any questions or comments you might have on our discussion forums. The full list of changes can be found in the full changelog. --- Installation Instructions The base compiler can be installed as an opam switch with the following commands: opam update opam switch create 5.5.0 The source code for the release is also directly available on: * GitHub * OCaml archives at Inria Fine-Tuned Compiler Configuration If you want to tweak the configuration of the compiler, you can switch to the option variant with: opam update opam switch create ocaml-variants.5.5.0+options where is a space separated list of ocaml-option-* packages. For instance, for a flambda and no-flat-float-array switch: opam switch create 5.5.0+flambda+nffa ocaml-variants.5.5.0+options ocaml-option-flambda ocaml-option-no-flat-float-array
Sacha Ayoun
@giltho.bsky.social

✅

rain 🌦️@sunshowers.io

Update: iddqd is now formally verified*! * with limitations that are fundamental to this kind of formal verification, making it a complement to the existing layers of validation For more, see: oxide.computer/blog/iddqd-u...

Sacha Ayoun reposted

rain 🌦️
@sunshowers.io

Okay, enough complaining. Soteria is actually quite awesome, and I've been able to prove some interesting invariants on iddqd with it. It is a tool in the toolbox -- it won't replace the extensive model-based tests -- but it can prove things across all possible kinds of adversarial inputs

rain 🌦️@sunshowers.io

Gosh I hate being reminded of how jank most language ecosystems are

Sacha Ayoun
@giltho.bsky.social

Thanks to everyone who came to our second edition of Caml in the Capital yesterday, we had a blast! Thanks to Jane Street for hosting us as well! #OCaml See you some time in September for the next edition

Sacha Ayoun
@giltho.bsky.social

I’m only learning about this today, fill this if you have time!

OCaml@ocaml.org

please participate in the OCaml Users Survey 2026, still open until and including May 25, 2026! link below

Sacha Ayoun
@giltho.bsky.social

The fact that there is no centralised hosting of packages for #OCaml means that if a single one of the 700 git hosts that my repo needs to ping to build a package is down, I'm not allowed to code today :(

Sacha Ayoun reposted

Anil Madhavapeddy
@avsm.amok.recoil.org.ap.brid.gy

Here's my proposal for voluntary disclosure of AI tool usage in published OCaml code. Are any other language ecosystems doing this? I'd love to hear about them if so! https://anil.recoil.org/notes/opam-ai-disclosure

anil.recoil.orgA Proposal for Voluntary AI Disclosure in OCaml CodeProposing a voluntary, machine-readable AI content disclosure scheme for OCaml spanning opam packages, dune, and per-module attributes, aligned with the W3C AI Content Disclosure vocabulary.
Sacha Ayoun
@giltho.bsky.social

The thing is entirely LLM generated from my previous website and cv, and from ingesting the entirety of the YOCaml tutorial which is apparently so well written that Sonnet 4.5 got made the website + CV in one shot after reading it

Sacha Ayoun
@giltho.bsky.social

Fun #OCaml fact. `ppx_expect` is designed to warn the user if they have a backtrace in their expected output. This is deeply annoying when... testing a library made for pretty printing backtraces 😭 I guess we're not saying "Called from here" but "Bananad from here" in our tests

You are up to date.