| When I was saying 'easier' if we chose to do logic inside a theory using the Curry-Howard correspondence then we find out that it is intuitionistic, and as you mentioned 'proofs' that means it may be important to you vs. someone who is say using lambda calculus as just a programing language. The Curry-Howard correspondence results in an isomorphism 'Programs'(Haskel Functions) and intuitional proof systems, if you assume they are traditional proofs internally you will have a bad time. What is important is what we lose in respect to what we often assume due to the typical conventions. Note that this has been a popular resource to introduce the concepts for a while, and I was encouraging you to mostly learn the tradoffs of call/cc to help on that path and avoid globals, not that it is the only or even good solution. > This course is an introduction to the research trying to connect the proof theory of classical logic and computer science. We omit important and standard
topics, among them the connection between the computational interpretation
of classical logic and the programming operator callcc. Grounding and negation as failure are also popular, especially with ML which under the VC dimensionality interpretation of learnability is still a choice function due to the set shattering. https://cdn.aaai.org/ojs/7590/7590-13-11120-1-2-20201228.pdf That said, I do retract my suggestion as you are in JavaScript, the obviousness in Scheme that callcc is external is not there. |