Conversation

Oooh yeah! Sounds similar to what declarative debugging is based on! I think there were papers on this on implementations for Haskell and Mercury.

Also related might be the interaction trees stuff for Coq (more from a proof perspective).

I think there the use case there iirc is proving stuff forall possible ‘traces’ of a effectful programs?

Nick Smith

@NickSmit_

The experience I proposed can only be built upon a declarative language, so there's a connection there. But I don't otherwise see a strong link to the research you've mentioned—it seems to be about a *better* debugging tool, whereas I'm saying we should mash everything together!

12:03 PM · Aug 26, 2022Twitter Web App

Replying to

@NickSmit_

Oh yeah, that's a specific use case definitely and far more limited compared to what you are proposing. More thinking these are different things based on this way of looking at programs… if that makes sense. Sorry!

Replying to

and

The ability to replay and stop and patch during a declarative debugging session in mdb (th mercury debugger) kind of reminded me of what you were talking about to some extent.

Nick Smith

@NickSmit_