Post #1846757

Replies (1)

• @jonmsterling@mathstodon.xyz 2026-04-30 13:29

  @cbaberle @MartinEscardo I'm open to it, but I need to see something that answers questions like “How do you turn a specification of an equational theory into something executable” that actually works — in the sense that 1. It needs to support eta laws / extensionality laws. 2. It needs to have competitive performance. 3. It needs to be complete. Drop any one of those three things, and the system is not fit for purpose. Unfortunately, this seems to be the part that almost everyone punts on. The work that got the furthest, in my opinion, was Andromeda — but I think the takeaway from that work was, also, that it is a problem that probably cannot be satisfactorily solved in general. Unfortunately, this is an area where you can't do almost anything until this problem is 100% licked. So, pending entirely new ideas, I'm continuing to bet on purpose-built systems vs. general frameworks/workbenches. It's really hard, because most of the time, the good algorithms for doing these things rely on our knowledge of metatheorems of various systems, and the “implementation" of those metatheorems as code. (For example, inverting type constructors up to judgemental equality.) There's a ton of deeply specific algorithmics that go into the implementation of even a very simple type system, I just don't see it being done satisfactorily in a generic framework.

  Open ##1846759