11 ms·
This is me! Didn’t expect to see this on here, but I’m looking forward to working with everyone else at the Lean FRO and the wider Lean community to help make L
by cwzwarich 2y ago
This is me! Didn’t expect to see this on here, but I’m looking forward to working with everyone else at the Lean FRO and the wider Lean community to help make Lean even better.
My background is in mathematics and I’ve had an interest in interactive theorem provers since before I was ever a professional software engineer, so it’s a bit of a dream come true to be able to pursue this full-time.
- brcmthrowaway 2y agoSurprised you didnt go into something AI adjacent
- adamnemecek 2y agoLean is AI adjacent.
- saagarjha 2y agoOnly because the AI people find it interesting. It's not really AI in itself.
- cwzwarich 2y agoIf you’re interested in applications of AI to mathematics, you’re faced with the problem of what to do when the ratio of plausible proofs to humans that can check them radically changes. There are definitely some in the AI world who feel that the existing highly social construct of informal mathematical proof will remain intact, just with humans replaced by agents, but amongst mathematicians there is a growing realization that formalization is the best way to deal with this epistemological crisis. It helps that work done in Lean (on Mathlib and other developments) is reaching an inflection point just as these questions become practically relevant from AI.
- mkl 2y agoIt's not AI in itself, but it's one of the best possibilities for enabling AI systems to generate mathematical proofs that can be automatically verified to be correct, which is needed at the scale they can potentially operate. Of course it has many non-AI uses too.
- ofrzeta 2y agoThey do have AI on their roadmap, though: https://lean-fro.org/about/roadmap-y2/ https://lean-fro.org/about/roadmap-y2/
- fspeech 2y agoIf you want to have superhuman performance like AlphaZero series you need a verifier (valuation network) to tell you if you are on the right track. Lean (proof checker) in general can act as a trusted critic.
- zozbot234 2y agoProof automation definitely counts as AI. Not all AI is based on machine learning or statistical methods, GOFAI is a thing too.
- trenchgun 2y agoIt's not ML, but it is AI
- fantod 2y agoI don't know what his reasons are but it makes sense to me. Yes, there are incredible results coming out of the AI world but the methods aren't necessarily that interesting (i.e. intellectually stimulating) and it can be frustrating working in a field with this much noise.
- uoaei 2y agoI don't want to come across as too harsh but having studied machine learning since 2015 I find the most recent crop of people excited about working on AI are deep in Dunning-Kruger. I think I conflate this a bit with the fascination of results over process (I suppose that befuddlement is what led me to physics over engineering) but working in ML research for so long it's hard to gin up a perspective that these things are actually teleologically useful, and not just randomly good enough most of the time to keep up the illusion.
- croemer 2y agoWhat do you mean by "things that are actually teleologically useful"? Fellow physicist here by the way
- Baeocystin 2y agoNot OP, but I'm assuming he means that they are maddeningly black-boxy, if you want to know how the sausage is made.
- uoaei 2y agoLike useful in an intentional way: purpose-built and achieves success via accurate, parsimonious models. The telos here being the stated goal of a structurally sound agent that can emulate a human being, as opposed to the accidental, max-entropy implementations we have today.
- calf 2y agoIs a guide dog teleologically useful?
- oulipo 2y agoThis is *VERY* AI-adjacent... the next batch of AI algos will need to integrate reasoning through theorem provers to go next level
- adamnemecek 2y agoWhat was the tipping point that made you want to work on Lean?
- cwzwarich 2y agoI don't think there was a single tipping point, just a growing accumulation of factors: - the release of Lean 4 slightly over a year ago, which impressed me both as a proof assistant and a programming language - the rapid progress in formalization of mathematics from 2017 onward, almost all of which was happening in Lean - the growing relevance of formal reasoning in the wake of improvements in AI - seeing Lean's potential (a lot of which is not yet realized) for SW verification (especially of SW itself written in Lean) - the establishment of the Lean FRO at the right time, intersecting all of the above
- a1o 2y agoHow does Lean compares with Coq? (I am not familiar with Lean but am familiar with Coq)
- denotational 2y agoMario Carneiro’s MS Thesis has a good overview of the type theory and how it compares to Coq: https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf https://github.com/digama0/lean-type-theory/releases/downloa...
- a1o 2y agoThank you!
- croemer 2y agoWe're you really _the_ creator of Rosetta 2? How big was the team, what was your role in it? Rosetta 2 is amazing, I'm genuinely surprised this is the work of just one person!
- cwzwarich 2y agoI was the only person working on it for ~2 years, and I wrote the majority of the code in the first version that shipped. That said, I’m definitely glad that I eventually found someone else (and later a whole team) to work on it with me, and it wouldn’t have been as successful without that. When people think of a binary translator, they usually just think of the ISA aspects, as opposed to the complicated interactions with the OS etc. that can consume just as much (or even more) engineering effort overall.
- croemer 2y agoThat's super impressive. I remember being astonished that the x86 executable of Python running through Rosetta 2 on my M1 was just a factor of 2 slower than the native version. QEMU was something like a factor of 5-10x slower than native, IIRC.
- lostmsu 2y agoQEMU probably had to account for differences in memory models. A fork with that stuff removed might be able to easily catch up.
- bonzini 2y agoQEMU loses a bit from being a generic translator instead of being specialized for x86->ARM like Rosetta 2, Box64 or FEXEmu. It does a lot of spilling for example even though x86 has a lot fewer registers than aarch64. Flags are also tricky, though they're pretty well optimized. In the end the main issue with them is also the spilling, but QEMU's generic architecture makes it expensive to handle consecutive jump instructions for example.
- steego 2y agoThis is exciting! Given your experience with Rosetta 2 and your deep understanding of code translation and optimization, what specific areas in Lean’s code generation pipeline do you see as ‘low-hanging fruit’ for improvement? Additionally, which unique features or capabilities of Lean do you find most promising or exciting to leverage in pushing the boundaries of efficient and high-quality code generation?
- cookiengineer 2y agoDo you have book recommendations in regards to disassembly, syscalls, x86/64 assembler etc? What do I need to know to be able to build something as advanced as rosetta? I am assuming that you reimplemented the syscalls for each host/guest system as a reliable abstraction layer to test against. But so many things are way beyond my level of understanding. Did you build your own assembler debugger? What kind of tools did you use along the way? Were reversing tools useful at all (like ghidra, binaryninja etc)?
- peterkelly 2y ago"Virtual Machines: Versatile Platforms for Systems and Processes" by Jim Smith and Ravi Nair is a great book on the topic.
- markus_zhang 2y agoThank you. Other than papers, I think this is one of the rare books that talk extensively about dynamic recompilation. I was hoping to learn more about the PPC M68K emulator (early version interpreter style and later version dynamic recompilation style) and definitely will read it.
- deleted 2y ago[deleted]
- singularity2001 2y agosorry to hijack the discussion but do you see any chance of consolidating the theoretical framework of real numbers with practical calculations of floats? That is if I proof the correctness of some theorem for real numbers ideally I would just use that as the algorithm to compute things with floats. also I was shocked to learn that the simple general comparison of (the equality of) two real numbers is not decidable, which is very logical if you think about it but an enormous hindrance for practical applications. Is there any work around for that?
- zozbot234 2y agoYou can use floats to accelerate interval arithmetic (which is "exact" in the sense of constructive real numbers) but that requires setting the correct rounding modes, and being aware of quirks in existing hardware floating point implementations, some of which may e.g. introduce non-exact outputs in several of the least significant digits, or even flush "small" (for unclear definitions of "small", not always restricted to FP-denormal numbers) results to zero. Equality is not computable in the general case, but apartness can be stated exactly. For some practical cases, one may also be able to prove that two real numbers are indeed equal.
- deleted 2y ago[deleted]
- markus_zhang 2y agoThank you! My work laptop is a M4 Macbook Pro so I really appreciate the beauty of Rosetta. Thank you for the effort! I just checked your LinkedIn and realized you joined Apple since 2009 (with one year of detour to Mozilla). You also graduated from Waterloo as a Pure Math Graduate student (I absolutely love Waterloo, the best Math/CS school IMO in my country - at the age of 40+ I'd go without doubt if they accept me). May I ask, what is the path that leads you to the Rosetta 2 project? I even checked your graduate paper: ( https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-806c18cc7811 https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... ), but it doesn't look like it's related to compiler theory. (I myself studied Mathematics back in the day, but I was not a good student and I studied Statistics, which I joked that was NOT part of Mathematics, so I didn't take any serious Algebra classes and understand nothing of your paper)
- flkenosad 2y agoWaterloo really is the best CS school in the world.
- markus_zhang 2y agoI have never been there, what do you consider to be its speciality comparing to say MIT and Berkeley?
- Me1000 2y agoDidn’t go there but worked with a lot of great folks who did. The main thing I think is that they require their students to get industry experience before they graduate. I don’t remember the actual requirement, unfortunately.
- markus_zhang 2y agoThanks, is it something different from coop? I checked their graduation requirement and it is indeed interesting: > Students admitted at the 1A level (except for those in Business Administration and Computer Science double degree), will normally have eight academic terms and six work terms. Six work terms seem to be a LOT. Most coops I know is just a few summers.
- mattgreenrocks 2y agoRosetta 2 is easily one of the most technically impressive things I've seen in my life. I've done some fairly intense work applying binary translation (DynamoRIO) and Rosetta 2 still feels totally magical to me.
- cwzwarich 2y agoThanks. It means a lot coming from someone with experience in our niche field.
- lenkite 2y agoCan Lean can do what TLA+ does - model check thorny concurrency problems ?
- yieldcrv 2y agoOut of curiosity, if you’ve been at a FAANG since at least 2009, have you ever retired or taken a “sabbatical” for a year or two, since you would have made enough money to retire and live passively at amounts similar to annual compensation and taxed way better Just curious how the decisions have formed, its totally fine if FAANG or specifically Apple was fulfilling for you, I also wonder if its financial fear to an irrational extent just because I see that on Blind a lot
- cwzwarich 2y agoI did go to Mozilla Research to work on Servo/Rust for a bit in 2015, which didn’t turn out to be the best decision. I always assumed that I would stick around at Apple until some singular event that would motivate me to quit, and that would be it. I have been so lucky at Apple to have been in the right place at the right time for several projects: relatively early iPhone team, original iPad team, involved in the GCC -> Clang transition, involved in the 64-bit ARM transition, involved in early Apple Watch development, first engineer working full-time on the Apple silicon transition for the Mac, etc. Obviously I was doing something right if I kept getting these chances, but if I went to another FAANG I wouldn’t have the same history, and I don’t think it would be the same experience. My projected path to parting ways with Apple didn’t really take place, since I’m now working at a non-profit dedicated to developing an interactive theorem prover and left Apple without any animosity in either direction.
- grecy 2y agoIt would be incredible if you could write a book someday about all those experiences. I would very happily buy that book. Thanks for all that incredible work and your insights here.
- markus_zhang 2y agoWow that's really a ton of memorable experience. I hope you write a book or some blog posts or do an interview.