9 ms·
Rosetta 2 creator leaves Apple to work on Lean full-time
- brcmthrowaway 2y agoWhat is Lean FRO?
- cwzwarich 2y agohttps://lean-fro.org/about/ https://lean-fro.org/about/
- hinkley 2y agoYeah that really doesn’t help.
- lambdas 2y agowe aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant https://lean-lang.org/ https://lean-lang.org/ Yep. Truly a mystery.
- aaravchen 2y ago~~Nice addition of a link that doesn't exist in the actual "quoted" source. If it did exist it would certainly be helpful though, so thanks for adding it I guess.~~ EDIT: Apparently their website design is just so poor their clickable links are identical to the non-clickable plain text. That link is a clickable word if you completely guess you can click on some of the apparent plain text.
- lproven 2y agoFWIW, not having done a proof since about 1982, it doesn't help me either.
- threeseed 2y agohttps://lean-lang.org/lean4/doc/ https://lean-lang.org/lean4/doc/
- croemer 2y agoThat answers the Lean part, FRO stands for Focused Research Organization
- swat535 2y agoThat doesn't say much.. Research on what? It looks like Lean is a programming language but everything else is pretty abstract to me.
- jemmyw 2y agoThere are a lot of broken links in the docs. Like most of the feature links.
- kmill 2y agoThere's a completely new language reference in the process of being written: https://lean-lang.org/doc/reference/latest/ https://lean-lang.org/doc/reference/latest/ (by David Thrane Christiansen, co-author of The Little Typer, and Lean FRO member) Some links here seem to be broken at the moment — and David's currently on vacation so they likely won't be fixed until January — but if you see for example https://lean-lang.org/basic-types/strings/ https://lean-lang.org/basic-types/strings/ it's supposed to be https://lean-lang.org/doc/reference/latest/basic-types/strings/ https://lean-lang.org/doc/reference/latest/basic-types/strin...
- bagels 2y ago"we aim to tackle the challenges of scalability, usability, and proof (Mathematics) automation in the Lean proof assistant."
- thih9 2y agoBackground about the organization: https://en.m.wikipedia.org/wiki/Convergent_Research https://en.m.wikipedia.org/wiki/Convergent_Research Their proof assistant / programming language: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
- yairchu 2y agoLean is a currently-niche programming language / proof-assistant. A proof assistant is basically a tool to construct mathematical proofs, which verifies that the proofs are correct like how a compiler verifies types in your programs. IIUC a regular programming language with a certain set of restrictions already duals as a proof-assistant as discovered by Curry & Howard. By restrictions, I mean something like how Rust forces you to follow certain rules compared to Java.
- cwzwarich 2y agoThis 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.
- evaneykelen 2y agoIn a previous discussion the name of Gary Davidian is mentioned who also — initialy single-handed — did amazing work on architecture changes at Apple. There’s an interview with him in the Computer History Museum archive. https://news.ycombinator.com/item?id=28914208 https://news.ycombinator.com/item?id=28914208 https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
- markus_zhang 2y agoFrom wiki it looks like David's emulator is perhaps uses interpreting as wiki says Eric's uses dynamical recompilation and Connectix' is even faster so maybe more optimization. I tried to find the source code of any without any success.
- lproven 2y agoAll this stuff is or was proprietary, closed-source tech, and what's more, it was tech that gave certain companies strong competitive advantage at particular points in time -- so they had strong incentives to make sure it did not leak. (I see posters in this thread who do not know what I thought were well-documented parts of the story, so I am trying to spell out the context here.) Some large reputable companies have histories of stealing other's code, ideas, implementation methods, algorithms etc. and passing them off as their own. IBM, Microsoft, Sun, Apple, Google, Oracle, Digital Research, Lotus -- all were dominant players, all were so accused. Most either backed down, or re-wrote, or re-implemented to avoid being sued. Microsoft more than almost anyone, and it only thrived because it was able to pay other companies off, or simply wait for them to go broke. Sometimes, how code works can be deduced simply by studying what it does. I worked out how Rsync worked because someone asked me to explain what it did in detail. Powerquest's PartitionMagic was amazing, black magic tech when it came out. I didn't review v1 because I did not believe what the packaging said; when I reviewed v2, a reader wrote in accusing my employers of doing an elaborate April Fool's joke and pointed out that my name is an anagram of APRIL VENOM. (If I ever branch out into fiction, that's my pseudonym.) Now, the revolutionary functionality of PartitionMagic is just an option in one screen of some installation programs. It's valueless now. Once people saw it working, they could work out how it was done, and then do it, and it ceased to have value. Very fast emulation is not such a thing. Setting aside sheer Moore's Law/Dennard scaling brute horsepower, efficient emulation during the short window of processor architecture transitions is a massive commercial asset. Apple has done it 3 times between 4 architectures. 68000 -> PowerPC PowerPC -> x86 x86-64 -> Arm64 Nobody else has ever done so many. IBM bought Transitive for QuickTransit, but it's not clear how it used it. Its major architecture change was IBM i. Originally OS/400 on AS/400, a derivative of the System 36 minicomputer, it successfully moved this to POWER servers. However, there is a translation layer in the architecture, so it didn't need Transitive for that. But IBM has bought many radical tech companies and not used the tech. E.g. Rembo, an amazing Linux-based boot-time network-boot fleet deployment tool it never really commercialised. Microsoft bought Connectix for VirtualPC, kept the disk formats and management UI and threw away everything else, because Intel and AMD bundled the core virtualisation tech. I know a little of the binary translation tech because the man who wrote it flew across the Altantic for me to interview him. All thrown away, but today, it's valueless anyway. At the time, though, very valuable.
- ein0p 2y agoApple just seems to be bleeding talent left and right. I wonder what's going on over there to cause people to leave when the job market is as uncertain as it is right now.
- raverbashing 2y agoCitation needed? I mean, there will always be long tenured people leaving, even without offers on the table Some jobs get old eventually
- blitzar 2y agoThe 20th million doesn't hit as hard as the 19th and when you make 2x your salary on the dividends on your stock you start to wonder why not just do something more interesting.
- tchbnl 2y agoSometimes people just want to work on cool stuff and have the luxury of being able to do that. Rosetta 2 is shipped and done.
- turnsout 2y agoYou could have posted this in 1985 and been right. Talented people have options.
- danielktdoranie 2y agoI am pretty sure “lean” is that codeine cough syrup rappers drink
- dilsmatchanov 2y agohttps://youtu.be/4Or-5OLCNDA?si=mzd_o0573HPgCVrl&t=51 https://youtu.be/4Or-5OLCNDA?si=mzd_o0573HPgCVrl&t=51
- hinkley 2y agoThe audio on this is about the worst I’ve ever heard on YouTube. I fast forwarded and at least he stops playing that loud music over his quiet voice, but damn. He gets off topic a lot (bullies, amphetamine salts??) and spends the entire time talking to the commenters not the video recording. Surely, there’s a better video out there than this.
- revskill 2y agoThe linkedin back button is weird. Instead of coming back to hn after back button, it goes to its homepage.
- Yujf 2y agoIts not weird its just disgusting. The back button should go back
- dirtysanchez 2y ago[dead]
- jviotti 2y agoHow is the Lean non-profit getting funded to be able to afford such great devs? How does that work in general?