[touisteur]

The authors work seems very interesting, and could maybe lead to the automatic generation of a language server with semantic query and refactoring capabilities, for any programming language. Or portable (in the 'language to language' sense) static analysis tools or interpreters or symbolic execution tools...

Just wondering (out loud) how you formalize language semantics so they can be consumed... I know about grammar formalisms (bnf/ebnf, antlr, peach/xsd/asn.1...) but what is the lingua franca of language semantics? Except for latex papers...

[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.