I am continuing to learn Lean (see part 1 and part 2). I lost some steam around March-April, but in the last two months I picked it up again. In a way it was a nice spaced repetition for relearning some of the basics. This summary was supposed to be my notes from finishing the rest of Mathematics in Lean and finishing chapters 2 and 3 of exercises from Terence Tao’s Analysis textbook, but also I couldn’t help also comment on the challenges and opportunties I see in doing formal mathematic...| Rado's Radical Reflections
Around 5-8 years ago when working on Angular and TypeScript rules in Bazel, I got very interested in exploring the core ideas of incremental computation, which seemed like the right way to abstractly (but still precisely) describe the similarities between build systems and UI reactivity. As an aside, incremental dataflow is a third view into the same concept, but I am least familiar with it. I wrote the following series of posts to try to pull all the different threads together. It was useful...| Rado's Radical Reflections
I am continuing to learn Lean (see part 1) by going through Mathematics in Lean. These are my notes as I just finished chapters one through five. Mathematics in Lean The online book is well-paced and well-written to connect with what an average student of mathematics already knows. The focus is on learning how to do basic mathematical proofs in Lean, and the underlying language is taught as needed for those goals, in comparison to Theorem Proving in Lean which is more of a language guide. For...| Rado's Radical Reflections
Incremental computation is a way of performing computations, with the expectation of future changes in the inputs to the computiation. When those changes occur the output can be updated efficiently, at minimum faster than redoing the whole computation from scratch. This problem occurs in many programming domains - UI programming, data flow, build systems, compilers, code editors. Likely you have seen it before, but didn’t call it incremental computation. Despite its prevalence, it is rarely...| Rado's Radical Reflections