it's amazing how much easier it is to think of it as a statement for "there exists" and "(for) every..." with examples
Conversation
Oooh, if you have got to generic functions, then you have an example of universal quantifiers in Rust! Although you can't disentangle them from 'type functions' so it might be a bit confusing… (ie. there's no way to write `<T, ...> -> U` on its own).
1
yeah but I think I also need to go over functions, domains, and codomains with him first because right now he's confused over notation where different quantifiers have been applied to a variable proposition right after one another
2
1
Heh, tbh I'm not actually famialar with the issues with teaching the logic notation, although I hear it can be a challenge to those quantifiers. I mainly learned logic etc. via Agda, Idris and Lean etc. 😳
2
Like, 'lambdas being the way to construct a forall/implication' helped me a bunch. Along with the logical connectives etc.
1
1
interestingly I couldn't understand any of it before I started formally studying math. I just glossed over it because I didn't understand it, and I wasn't interested in it
1
1
I haven't done any functional programming really but when I do it sometimes in Rust, I actually completely understand what I'm doing only because I started learning and doing lots of math. I didn't really get it before
2
1
Would highly recommend playing around with Agda, Coq, or Lean some day, if you get the chance! They're amazing and super cool.
1
1
yeah I actually have a really tricky algo design problem that we've put aside that I've been thinking of formalizing in e.g Coq (I've no experience with it so unsure how it can be done yet)
1
1
Oh nice, if you ever want to chat about it, let me know! I've only done really basic stuff though, like proving the correctness of an arithmetic expression compiler… Software Foundations has a bunch of good stuff it though (I've only done bits of it however)
2
1
Have you looked at model checking? That might be easier, but it could depend on the problem. Another approach would be to use a solver like Z3, if it works.