221–230 of 230 posts
Is it possible that small bugs or assumptions in a root paper could cascade through referencing papers leading to wildly inaccurate outcomes 5 or 6 papers down the line?
https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
Earlier quoted context omitted.
Yes. Not knowing who Terry Tao is,, if you're on HN, makes you an outlier.
Hi, it's me, I'm the outlier, it's me
Earlier quoted context omitted.
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.
(1) is the generally accepted meaning. The others need different words.
The latter would be a bad thing.
Earlier quoted context omitted.
5 months ago - a friend wrote me a python script and sent it to me...i couldnt get it to work. Used phind.com to explain what to do...it worked out my windows environment variables needed to be changed, told me how to structure a folder schema to place the src script...mindblowing stuff. And i have been using it - when it turn the same friend told me to write a similar script in python myself...it has been amazing to…
I am not going to visit the website you just posted here unless you explain how the mechanism works, otherwise I will assume it's just crappy advertisement in this post.
I understand your skepticism (because the internet is fully broken right now/and forum posts are more or less paid for content at this point)
but...its a bit funny you'd like someone who just explained they're a beginning programmer who got into programming because an LLM helped remove insane amounts of friction from the learning process to "explain a mechanism" to them.
Earlier quoted context omitted.
gpt4 is amazing, i rarely use google as as starting point for my programming related queries these days.
Google has actively become catastrophically bad to the point that it will ignore the only special keyterm I deliberately looking for for more general dumb results.. like it is literally unusable - I used to be able to find that very specific stackoverflow answer I have read years ago, or some barely read blogpost, and now I’m happy if it actually finds the website if I search for the domain name.. GPT would be good a…
Earlier quoted context omitted.
Noob here, how is Lean4 different from TLA+ or Alloy? Is that even a reasonable comparison? Edit: Wrote Allow the first time, good stuff.
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…
Earlier quoted context omitted.
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…
Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`. 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.
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…
I like ChatGPT’s answer better than yours. Rust’s cost generics and C++ aren’t dependent types in any sense. And saying “the type of one variable can depend on the value of another” is vague but a good intuition pump. Since I guess we’re doing dependent types explanations I’ll give it a go. Dependent types extend a type system with two new type thingies: 2-tuples where the type of the second element depends on the va…
> Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, you can also reasonably have dependent refinement types, like "type of all numbers greater than n".
Earlier quoted context omitted.
Saying Terence Tao is a math prof at UCLA is like saying John Carmack is a programmer at Keen Technologies.
If you're going for a PhD or researching some obscure, furthest reach study of some mathematical principle and you get stuck. One of the ways to move forward is to hope that Terence Tao finds your topic interesting and can give you a few minutes of his time - because he'll probably have some ideas for moving your research forward.
Perhaps I should try sending him a mail
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…
It's of course fine to ask chatgpt. I also appreciate that you wrote that it was from chatgpt. 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 Inter…
Yea that got lost on me. I think I view these things a bit differently than most on HN. I've noticed in general that the more I'm not at uni, the more my thinking has become heuristic and quick-ish. It used to be more thorough and in-depth. The trade-off of it being that such type of thinking is more time consuming but the answer is more comprehensive and/or accurate.