Lean Proving

Reading

• I’ve been reading Lean Prover along with Haskellbook. Lean Prover was advice from my friend, Lyle, who runs the PDX FP group. In terms of Haskellbook, I’m doing about a chapter a week (or two weeks depending on the week), starting out with the first. It gives me enough time to really get into Lambda Calculus. I’ll be doing this on the evenings, after plugging through my Nanodegree during the day.

• There seems to be two versions; one that has a Chapter 3 on Dependent Types, and the one I’m working through. Oh well.

• I know to some it’s not important, but considering it seems like I’m definitely on the path of becoming a proof engineer, and I like it (I shudder to say this, but many times more-so than my data-analysis stuff), I’ve been giving it a go.

• Data Science appeals to me on a lot of levels (Julia, Python, which I both love, and general stats), but at the same time, I’ve been hugely drawn by just types and how things work, and just proofs in general. And data is just not as interesting. Maybe I’ll find some way to include it as I continue to study. Numerical computation is more interesting than Data Science (to me), though! I can see why (with the PLT and numerical computation and interest in types) I am drawn towards languages like Julia and Haskell (and Python). But Data Science can be a bit tedious; you’re essentially doing the same thing over and over and the data is questionable. Some argue that it isn’t even a real science because it’s not truly reproducible. I have no comment on that, but since I first stumbled upon that comment, I’ve been thinking about that. In particular, Science being defined as doing research to advance a field based on reproducible experiments. Anyways, Numerical computation /verification / proofs has a bit more of a specific type of puzzle-solving that I really enjoy.

• It’s very difficult to delineate between such subtleties. Oh, I’m also finally making my way through Dana Scott’s LambdaConf videos on Lambda Calculus. They make so much more sense, having spent some time on SKI, etc. And I’m quite pleased he used a bit of Mathematica! :D I unfortunately was in Spivak’s Category Theory class, so I wasn’t able to attend this one in person. However, I had met Dana at POPL, and hope to meet him again later this year.

Proofs

• I’m still learning how to prove things, but I’d like to become better at lambda calculus, beta and eta reduction in general. Substitution and Reduction.

• I learned about ex falso sequitur quodlibet, which means “anything you want follows from falsity”.

• So I did a bit of this today. The puzzles are really interesting!

Some things

• I’m thinking of doing Intro to Mathematical Thinking again. The neat thing about the course is that you can take it many times. Or even the Hoare Logic one I took a while ago.

• I heard we have to write a COBOL programme for class :D Hilarious.

• I started reading Denotational Semantics (by Stoy) and saw this awesome video by Erik called “The Lost Art of Denotational Semantics”. Definitely worth checking out both! I ended up staying up for 2.5 hours thinking “I’ll just read a few pages”. It’s super engaging and I ended up carrying it around with me to read during my commute!

Things to do

• Lean Prover work through
• Nanodegree Project 1 complete between this week and next week
• Quiz for class (easy; can complete that tonight)
• Haskellbook one chapter a week (or two weeks depending on the week)