It’s been 3 months since my previous post about learning Lean part 3, so it’s time to write another one. I have mostly continued to work through Tao’s Analysis book through his excellent companion - which means all proofs from the paper textbook are fully formalized in Lean, while examples and exercises are stated in Lean but left with a sorry for me to fill in. Altogether the companions has close to 2000 sorries to fill-in.| Rado's Radical Reflections
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