Well it's too little to understand immediately but you can definitely come to grasp this stuff. There are a lot of mathy words here that do warrant their invoca

Well it's too little to understand immediately but you can definitely come to grasp this stuff. There are a lot of mathy words here that do warrant their invocation but don't mean that the math is arcane. You seem like you're interested which is all that matters. I'm going to be slightly handwavey/generalize here but I think it may be helpful. Predicate Logic is the basic logic that humans think of when they think "logic." It's, if-this-then-that style thinking with only basic "tools". Predicates are statements that can lead to other statements, for instance the predicate "it's raining" could imply the predicate "I will wear a jacket." You can even combine predicates such as, if "I'm hungry" _and_ "I have food in the fridge" then "I will eat." Typically, we use symbols instead of sentences so it will look more like (A and B) -> C. Assuming you've done some programming, you're already used to predicate logic in the form of if-else statements. You've also been exposed to type theory. I think SICP is in scheme so types are a little bit hidden but if you've programmed any of the modern non-lisp languages i.e. Python, Java, C, etc. then you've seen types. Types are ints, floats, strings, etc. You know how you can add two numbers but you can't add a number and a string without special rules? (1+1 == 2 but "cat" + 1 == ???) Type theory concerns these rules and a bit more. A question that type theory helps answer is, what are we permitted to do with certain classes of objects? Once the blog post gets into dependent types, I think it becomes a bit tricky to pick up. Dependent types are types that "depend" on other information. For instance, we might have a type called array which is a sequence of numbers of any length. We might further have a dependent type called the PointTripleArray := Array<3> i.e. it's an array with 3 terms and they type of PointTripleArray is the dependent type. There are other more complicated ways to use dependent typing but I'll skip those. Honestly, I kind of understand the rest of the post but not well enough to start explaining here. I wish I could. I think this is enough to get you started reading and learning though.