@ekaitz_zarraga If you are interested in the topic I can recommend you an interesting book, it's called "The Little Typer", from the creator of "The Little Schemer", maybe you know the book :)

I wish I had a friend who knew grad-level math and CS to talk or ask them many things

@ekaitz_zarraga in what things are you most interested in? :D

@ekaitz_zarraga are you into proof assistants?

@ekaitz_zarraga Coq is a proof assistant, it implements a type theory called the Calculus of Inductive Constructions (I don't know how is it). But in Coq it's not that easy to see that when using it because it uses "tactics" that are like an abstraction to prove things more easily. In another languages like Agda you can see that correspondence better.

@ekaitz_zarraga ohh, proof assistants are tools for proving properties about programs, theorem, etc., but machine-checked, so you can be 100% sure of the correctness. They are usually (or at least the ones I'm interested in) based in a type theory (like lambda calculus) and in the Curry-Howard corresponce, which is an equivalence between programs (in functional programming) and proofs. For me it's very interesting but these days I don't have many time to deep more :(