Is there value in learning verified programming for application developers? I've always been curious but they mostly seem like tools for academics.
Lean4 helped Terence Tao discover a small bug in his recent paper
141–150 of 230 posts
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#142Earlier quoted context omitted.
I'd say TLA+ is designed more for software people trying to design systems, write down specs, and reason about how the thing behaves dynamically. Lean is used mostly for writing down math proofs, and a lot less for software (although by the Curry–Howard correspondence, math proofs and programs have an equivalence, so the line is a little blurry). Lean has "mathlib", which is like a standard library of formally verifi…
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).
Yeah, I believe they said they intend for it to be used as a general purpose programming language. I used it to complete Advent of Code last year.
There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 )
Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 )
And I'm impressed that you can add to the syntax of the language, in the same way that the language is implemented, and then use that syntax in the next line of code. (paper: https://lmcs.episciences.org/9362/pdf ). There is an example in the source repository that adds and then uses a JSX-like syntax. (https://github.com/leanprover/lean4/blob/master/tests/playgr... )
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#143Earlier quoted context omitted.
I'm relieved that Lean4 doesn't seem to be some AI thing.
Automated reasoning is usually included in AI (Lean4 has tactics so it qualifies as such) but it's also quite different from the ML stuff that's the more usual kind of AI these days.
You can have both!
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
https://arxiv.org/abs/2306.15626
(shameless plug)
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#144Earlier quoted context omitted.
For the HN crowd, explaining who Terrence Tao is would be ike explaining who Obama is
This may be hard to believe, but a lot of us here in "the HN crowd" have zero interest in celebrity and do not keep a catalog of them all in our heads. Even intellectual ones. There's nothing wrong with that, but it's also just its own interest one or may not have. People approach things in a lot of different ways and it would be nice if we can just respect that instead of digging on each other or making unfounded as…
I don't have much interest in celebrity either, but I feel that you're short-changing Terence Tao. He's not really famous due to being celebrated, but he's celebrated due to his level of skill and breadth of mathematical knowledge (sometimes known as the Mozart of Mathematics).
I think your sentiment is misplaced as I would expect HN commenters to have heard of Tao as he often features in posts about mathematics. I'm sure I recall seeing some comments from him too.
There's an approachable Numberphile video featuring him here: https://www.numberphile.com/videos/the-worlds-best-mathemati...
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#145Earlier quoted context omitted.
So that's an excuse for such a low context post?
For the HN crowd, explaining who Terrence Tao is would be ike explaining who Obama is
I started to agree with you, but let's keep in mind that there are new generations of tech geeks out here who are just learning about the things we live and breathe.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#146I found a "bug" in one of Terence Tao's math blog posts too, years ago. I told him about it, he fixed it, and thanked me. I didnt make the front page of Hacker News, of course. lol
If anyone interested, I went into more detail about it, over in a post on my blog:
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#147Earlier quoted context omitted.
It's correct that he is a professor at UCLA, but it's also worth mentioning that he's regularly called nicknames like 'greatest mathematician alive' (just try googling that phrase): https://academicinfluence.com/rankings/people/most-influenti...
What would make him greater than other fields laureate?
Other mathematicians opinions of him and his work. He's very prolific and was considered a child prodigy.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#148Earlier quoted context omitted.
Tao got his PhD at the age of 21 and a tenured professor chair at the age of 24. To compare, at the age of 21 ordinary people only get their bachelors and typically it's 23-24 they when they get their masters degree. A PhD takes several more years and of course very few become tenured professors even more years later.
Dumb question: how do people skip years like this in college. Like suppose you do know the material well already, does that just get recognized by the faculty at some point (you are noticed pre-college and get a faculty member interested in you? In college?) or would he have needed to specifically apply for that in some way? I ask in jealousy, I felt like my college put as many administrative barriers as possible to…
In the 90s I sort of attended two universities at the same time in Hungary (given the time and the place it's not as big a deal as it sounds) and I said to the second one, hey I know the basic stuff, let me attend the more advanced one and they said, sure, no skin off my back, do whatever you want, if you fail, that's a you problem but if you pass the more advanced tests we will credit you the basic stuff.
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#149For 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…
[deleted]
Re: Lean4 helped Terence Tao discover a small bug in his recent paper
#150Earlier quoted context omitted.
I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fai…
Because I had the question and I figured this was quicker. I didn’t know what dependent types were. So now you know why I do it. Also, I believe this is my first time doing it. I might be wrong. Is it better to ask and wait for an answer instead? There is nothing in the guidelines on HN about it. I don’t know what’s reasonable and I haven’t seen strong cultural norms from HN yet. I at least labeled that the text was…
Did you forget about search engines that enable you to do your own research rather than asking a human or an LLM?