Any redex wizards in the room? I’ve modeled a language design on paper and want to use redex to explore / prove interesting properties, like I might with CoQ. I prefer to model “reductions” as judgments, as in Pierce’s TaPL.

I’ve got a grammar compiled and can write a simple judgment, but it’s not clear what to do afterwards.

So far, I’ve figured out how to use #:binding-forms and #:refers-to to make substitute work properly.

I guess you’ll want a metafunction to reduce terms to values

and then write tests to see that evaluation works like you expect

here’s what I’m working with (define-language lambda [t ::= (λ (x) t) (t t) n x] [v ::= (λ (x) t) n] [n := number] [x ::= variable-not-otherwise-mentioned] #:binding-forms (λ (x) t #:refers-to x)) (define-judgment-form lambda #:mode (steps I O) #:contract (steps t t) [(steps ((λ (x) t) v) t*) (where t* (substitute x v t)) "E-AppAbs"])

is this a typo: [v ::= (λ (x) t n)]

no, that’s a single-var abstraction

Can I make progress with a judgment of this form?

oh

wait

yes

ok

well the next things I’d do are: (1) write tests with redex-match? and (2) write tests for steps

fixed the typo. Sorry, losing sleep over this

(with judgment-holds)

ok cool, so redex-match? will generate test cases automatically, like haskell quickcheck?

no

oh, then it matches a pattern against a term

i see, the “curried” version of redex-match is for efficiency

yep. I think there’s a way to use redex-check though

maybe (redex-check lambda t (redex-match? lambda t))

(I usually write tests by hand)

Neat, redex-check will search for counter-examples at least.

I’m curious, what is redex intended for?

modeling!

quickly build a language, judgments

and test that everything works like you expect

then later, you can add new features to the languages

*language

and test that you didn’t break anything

Could I use it to prove my model is sound?

no

but you can test soundness

and yeah, coq on the other hand would help you prove soundness

I see. Hence the “practical” qualifier?

but you have to do more work to get that

yep

cool, thanks @ben!

it would be great if someone extended redex to prove coq-like theorems

but I’m not sure I would use it as much as “basic redex”

(because no matter what, there’s usually a big gap between the model & actual language, so I just want a model that’s quick and easy to work with)

I’ve got a use case or two in mind

At this point in a project (too much mess, time to fix some structure), I have to transition from Racket to Haskell or CoQ.

@ben did we ever consider not distinguishing between mutable and weak hashes at the type level?

Neither is ideal because they have entirely different sets of quirks that won’t matter back in Racket land.

no, I don’t think so

Sometimes, there’s too much friction to return to Racket land, which is tragic.

so you’d want to be able to use redex instead of coq?

short answer, yes

I want the benefits of types and ~inductive logic~ structural induction, but without the overhead of multiple toolchains. I was hoping to use Redex models to explore the language design as it evolves.

Found a tool called Ott (http://www.cl.cam.ac.uk/~pes20/ott/top2.html) that does something like what I thought redex would

Except more racket-y, like output to scribble