201–210 of 230 posts
For people that know neither (like me 5 minutes ago): >Lean4 > Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. https://lean-lang.org/about/ > Terence Tao > [...] is an Australian mathematician. He is a professor of mathematics at the University of California, Los Angeles (UCLA), where he holds the James and Ca…
Field's Medal winner.
Earlier quoted context omitted.
Leo de Moura wants Lean 4 to be used for software verification too. A cool thing about Lean 4 is that it's also a programming language, using the same syntax as for proofs, making it easy to consider proving correctness properties of programs you write. Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).
> Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs). Do you have to actually prove a tactic work for it to be sound? A tactic will rewrite the program into a simplified program that will verified by a kernel; if the tactic wrongly expands something, the kernel will later reject the program. Only the itself kernel need to be verified for the…
Is there a way to do lightweight incremental proof checking in a typical say Python or Javascript codebase? Maybe specifying some conditions/assertions in comments and have it verified using some static analysis tool? Though I recognize it could be quite a challenge in dynamically typed languages.
Python's Deal library provides contracts and a small portable formal proofs area of the codebase. Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered. It just works surprisingly well for incrementally building up provable code properties.
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
gpt4 is amazing, i rarely use google as as starting point for my programming related queries these days.
GPT would be good as a search engine, but who would want a search engine that stopped indexing a few years back? Also, it is not good at ultra niche topics, which would be the whole point of a search engine.
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people
They’re an easy 100x for the elite. Top engineers are now 10000x’ers.
Like if the answer is not a leetcode/CRUD code sample you can easily find on the internet either way, it can’t do anything useful. Like, my problems mostly constitute things like reasoning about the correctness of a given change in the context of the whole codebase, its threading model, etc. It will at best regurgitate some bullshit like “race conditions can be this and that” here, not helping at all.
For people looking for an easy introduction to Lean4, the Natural Number Game is great: https://adam.math.hhu.de/#/g/hhu-adam/NNG4 And if you just want to read without playing a game: https://lean-lang.org/theorem_proving_in_lean4/introduction....
Noob here, how is Lean4 different from TLA+ or Alloy? Is that even a reasonable comparison? Edit: Wrote Allow the first time, good stuff.
Do correct me if I’m wrong, but Lean is more about total functions/FP code, not sure how well does it handle threading, if at all. It might be more related to the correctness of the actual implementation of a serial algorithm.
Lean4 looks like a great language. Has anyone used it in production capacity for "normal" products/applications?
One reason for lack of adoption is that the verified standard library for programming is still rather small. Fortunately, it is expected to grow much more quickly now that there are developers who are getting paid to work on it and I expect that we will likely see a lot more on this front in the coming years.
Earlier quoted context omitted.
Huh, I can't seem to get in the groove of using it, maybe I'm old or something, but it annoys me all the subtle ways it's wrong and I feel I have a much better grasp if I think through it myself supported by Google.
I get a lot of mileage out of ChatGPT just treating it like an intern who turns around work instantly. You don't expect interns to write perfect code, but they can save you a ton of time if you set them loose on the right problems. For any relatively simple task I can say "Write a Python script to do X" and it will almost always spit out working code, even if it has subtle mistakes. Fixing mistakes is fine and part o…
Earlier quoted context omitted.
As someone who uses ChatGPT4 pretty much nonstop all day (I have a monitor dedicated to it) - it's almost certainly a 10-20x in fields I have no knowledge of (writing in languages I've never used, dealing with OS/Kernel/Network constructs that are unfamiliar to me) - I can knock off in an hour what might have taken me a day or two previously - but I don't think I've ever had a task where I could say that I completed…
The idea of the 10x programmer can mean 1) someone who produces a ton of code quickly 2) someone who can solve seemingly-intractable problems 3) someone who’s presence on a team improves everyone’s productivity quite a bit 4) someone who chooses technical decisions that save a ton of time down the line.
He started learning lean4 with the help of GPT4 just at the start of the month: https://mathstodon.xyz/@tao/111208692505811257 Many of his mastodon posts this month have been about his learning progress. Certainly an interesting case study of how LLMs can accelerate the work of even of the most extremely successful people