[aseipp]

Most people formalize "kernel languages" that contain all the bare essentials of the language at hand. There are a variety of tools to do this; a lot of people just end up embedding their language semantics in Coq or something and writing proofs about the theories there. Alternatively, a lot of people will tend to just write literal interpreters for their kernel language in a language like Haskell or OCaml; interpreters can be seen as a lightweight machine-runnable definition. And they have the added bonus you can play with them!

Another popular tool I'm aware of for this is Ott[1], which lets you write a high-level semantics description, much like you'd write in a LaTeX paper. It can then compile it to Coq, LaTeX, etc for further work. Ott is probably a much better place to start without getting too far into the weeds, if you want to write real high-level sketches.

In general, I (unfortunately) don't think there's anything like a "library" of language semantics definitions that are easily reusable or anything like that. Modular definitions of semantics that can be reused like a library/API is basically a programming language abstraction problem, but I'm not sure what the current forefront of research on that is. In general, very few languages have fully specified machine-checked semantics, or even unproven ones.

[1]: https://www.cl.cam.ac.uk/~pes20/ott/

[touisteur]

By the way I kept going down this rabbit-hole and found an example of what you described : https://unsat.cs.washington.edu/projects/serval/

IIUC Serval uses an interpreter built in Rosette (?) to build a Symbolic execution tool.

[touisteur]

Thanks a lot for this answer and the references.

I think the author is working on a generic semantic tool to generate all kinds of language tooling automatically ; I'll be sure to follow his work.