Yes, I’ve heard of Idris (I don’t know it, but I’m a fan, I’m looking into Coq for this project). I’m also already a massive fan of your work on CEAs, I believe I emailed you about it a while back.
I’m not sure I agree with you about the DSL implementation issue. You seem to be mainly citing development difficulties, whereas I would think that doing this may put a stop to some interesting features. It would definitely restrict the amount of applications. For instance, I’m fully considering Pedant to be simply a serialization format for Causal. Which would be difficult to do if it was embedded within an existing language.
Making a language server that checks for dimensional errors would be very difficult to do in a non-custom language. It may just be possible in a language like Coq or Idris, but I think Coq and Idris are not particularly user friendly, in the sense that someone with no programming background could just “pick them up”.
I may be interested in writing your CEAs into Pedant in the future, because I find them very impressive!
Hello Michael!
Yes, I’ve heard of Idris (I don’t know it, but I’m a fan, I’m looking into Coq for this project). I’m also already a massive fan of your work on CEAs, I believe I emailed you about it a while back.
I’m not sure I agree with you about the DSL implementation issue. You seem to be mainly citing development difficulties, whereas I would think that doing this may put a stop to some interesting features. It would definitely restrict the amount of applications. For instance, I’m fully considering Pedant to be simply a serialization format for Causal. Which would be difficult to do if it was embedded within an existing language.
Making a language server that checks for dimensional errors would be very difficult to do in a non-custom language. It may just be possible in a language like Coq or Idris, but I think Coq and Idris are not particularly user friendly, in the sense that someone with no programming background could just “pick them up”.
I may be interested in writing your CEAs into Pedant in the future, because I find them very impressive!