151–160 of 230 posts
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
Earlier quoted context omitted.
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?
It all has trade offs.
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…
some claim his intelligence is the highest ever measured
Is there value in learning verified programming for application developers? I've always been curious but they mostly seem like tools for academics.
For app dev I'd say the main problem is always "what we even need to build?", and then polishing over user experience.
Earlier 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…
However, I wouldn't recommend posting the result here if you don't know if it's correct. Moreover, anyone can ask chatgpt themselves. It's better to wait for someone here to post an answer.
Yes, there's nothing in the guidelines, but they're (deliberately) not all-encompassing. Besides, I would hope it's part of basic Internet etiquette; just because we now have access to tools that generate plausible-sounding but not necessarily correct answers to questions doesn't mean we need to post what they create in the place of genuine answers.
Earlier quoted context omitted.
Did you forget about search engines that enable you to do your own research rather than asking a human or an LLM?
I could use google but chatgpt wins on speed and asking on HN wins on vine. When someone asks me a question I am mostly quite enthusiastic in explaining it. You can’t get that as easily from a search engine. It all has trade offs.
Earlier quoted context omitted.
Tests only show that it is correct for the sets of values and code paths you exercise. It's quite possible for other aspects to be incorrect, and this is what theorem provers like Coq help with.
If you have an incomplete or buggy specification Coq won't actually prove the absence of bugs.
Earlier quoted context omitted.
Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.
Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point? What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was…
You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).
Earlier quoted context omitted.
Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model. C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checke…
Formal verification is often not the best tool for ensuring code correctness from an ROI perspective. Things like unit tests (including property based tests) and ensuring 100% code coverage often achieve adequate results with less effort.
Tangent useless comment: while checking this Mastodon instance, I noticed a specific user is spamming the global feed by replying to his own posts every other day. I only saw his posts, mostly, and wondered if this was a personal instance of sorts.