but I wouldn't start introducing the math background to a beginner unless they expressed an explicit interest in it, because if someone wants to just program, they don't have to have it. one of my very strong beliefs is that you have to just do a lot of programming to get better.
Conversation
anyway I love teaching and I really want to teach one day for money at an university level, thank you for coming to my TED talk
1
2
what's interesting is that in most estonian textbooks the existential and universal quiantifiers are explained in such a dry way that it's no wonder he didn't understand it. they just throw the definitions into the text and don't explain it.
2
2
it's amazing how much easier it is to think of it as a statement for "there exists" and "(for) every..." with examples
1
2
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
Replying to
Would highly recommend playing around with Agda, Coq, or Lean some day, if you get the chance! They're amazing and super cool.
Replying to
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
Show replies