@pocmatos: Thank you for reading my article and for the kind words. I might revisit the topic and talk about PLT Redex for programming languages—I’ll let you know when that happens. I learned what I know about Redex from the following sources: https://mitpress.mit.edu/books/semantics-engineering-plt-redex http://www.eecs.northwestern.edu/~robby/lightweight-metatheory/ https://docs.racket-lang.org/redex/index.html https://redex.racket-lang.org/ https://dvanhorn.github.io/redex-aam-tutorial/

@leafac I saw your post too, and liked it a lot. Thanks for writing it!

@pocmatos: I find these resources great, by the way. Along with the rest of Racket’s documentation, it not only shows what you can do with the tools, but also help fill the gaps on the theoretical background necessary to follow the discussion. For example, Part I of Semantics Engineering with PLT Redex is about theory. Also, you can always ask questions here, if there’s something you don’t understand.

@robby: Thank you very much for reading and for your kind words :slightly_smiling_face:

BTW, a fun exercise that I think is also illustrative along those lines is to take values like this:

(define-language L (v ::= (b …)) (b ::= 0 1))

(with some other stuff)

and then implement a language that can do addition

there are a bunch of ways to go about that and they lead to interesting tradeoffs.

For example, here’s one way to do and:

(--> (and (b_1 …) (b_2 …)) (concat (and (b_1) (b_2)) …))
(--> (concat (b …) …) (b … …))

where you then add the three (or so) rules that cover how and works on single element vectors.

that set up looks nice until you try out some examples and you see some oddities in the reduction graph.

anyway, thanks again for the well-done post.

@robby: It took a while for me to understand what you said :slightly_smiling_face: First of all, I didn’t know (--> (concat (b ...) ...) (b ... ...)) was a thing. It’s so nice! I just changed a metafunction I had here to use this :slightly_smiling_face: I can’t see what kinds of oddities one would find in the reduction graph. Can you please expand a bit?