creata

15 ms·

241.
by creata 1y ago
This. Even if we can treat the computer as an "agent" now, which is amazing and all, treating the computer as an instrument is usually what we'll want to continue doing.
242.
by creata 1y ago
Merge sort in Dafny: predicate sorted(a: seq<int>) { forall i, j :: 0 <= i <= j < |a| ==> a[i] <= a[j] } predicate merge_invariants(a: seq<int>, b: seq<int>, c: array<int>, i
243.
by creata 1y ago
True! Rust proves that you can get very far while only rarely using unrestricted shared mutable data (UnsafeCell). Do you know anything that uses borrowing-like ideas in a theorem proving context?
244.
by creata 1y ago
In my uninformed opinion, the difficulty with code extraction (or going the other way, extracting a theorem prover representation from a program) is shared, mutable data. All the solutions I've seen (e.g., separation logic) feel clunky
245.
by creata 1y ago
> Formal systems may be easier than React to understand Some specific formal systems, maybe. I feel like a lot of people could get some mileage out of learning Dafny, and it'd definitely be easier than learning React imo.
246.
by creata 1y ago
The subsections / follow-up questions repeat too much information that has already been explained. I don't think this has the kind of well-paced progression of concepts that you'd want for learning anything efficiently. The a
247.
by creata 1y ago
> Further C# has destructors that get used as a last resort effort on native resources like file descriptors. True, I was going to mention that, but I saw that JS also has "finalization registries", which seem to provide finali
248.
by creata 1y ago
C# has the advantage of being a typed language, which allows compilers and IDEs to warn in the circumstances I mentioned. JavaScript isn't a typed language, which limits the potential for such warnings. Anyway, I didn't say it was
249.
by creata 1y ago
This seems error-prone, for at least two reasons: * If you accidentally use `let` or `const` instead of `using`, everything will work but silently leak resources. * Objects that contain resources need to manually define `dispose` and call i
250.
by creata 1y ago
> a better library ecosystem For what it's worth, Erlang's standard library is decently "batteries-included". The C interop also isn't terrible.[1] [0]: https://www.erlang.org/doc/apps/s
251.
by creata 1y ago
Honestly, I doubt that LLMs are great for learning. Too often, they output plausible-sounding things that turn out to be completely wrong. I know Wikipedia can have its problems with factuality, but this is on an entirely different level.
252.
by creata 1y ago
C and Rust both tend to be more sane than C++, though, so you can't just pin it on C++ being a systems programming language.
253.
by creata 1y ago
Can you state more clearly why it's deeply flawed? Because while LLMs obviously have massive limitations, so do humans, and it's not entirely clear to me that some synthesis of the two can't produce much better results than
254.
by creata 1y ago
Even o4-mini (free) uses web searches and runs Python scripts very eagerly. I'm not sure how long they'll be able to afford giving all of that away.
255.
by creata 1y ago
> at this point I wouldn't recommend React at all. Out of curiosity, what would you recommend?
256.
by creata 1y ago
That's a good point, thanks. I interpreted "sell you the cure to the disease they created" as selling it to the public, but I'm sure advertisers would love to make Fifteen Million Merits a reality.
257.
by creata 1y ago
Have you seen this scenario ("an expert AI engineer and therapist working together" to create a good therapy bot) actually happen, or are you just confident that it's doable?
258.
by creata 1y ago
Justifying what Worldcoin is doing by comparing them to black market leaks isn't helping their case.
259.
by creata 1y ago
> the only way you'll be able to tell if you're talking to a human is with... Or the tried-and-true method of trusting only friends, friends of friends, recommendations from friends, etc.
260.
by creata 1y ago
Maybe it would allow you to rate-limit and/or ban by the human, which is probably more effective than banning by IP address. (Obviously Worldcoin is shady as shit, I'm not defending it.)
261.
by creata 1y ago
Or maybe they have experienced what it was like and they don't want to go back.
262.
by creata 1y ago
> That's not why people use LaTeX. Many people say that they use LaTeX because it produces more beautiful output. Microtypography is one of the reasons for that. It's especially noticeable when microtype pushes hyphens or quote
263.
by creata 1y ago
I could deal with all of the other issues if it weren't for the absurdly long compile times. I wonder where most of that time is spent.
264.
by creata 1y ago
Oh true, section breaking is also important. And figure placement. Things like default margins, in my opinion, are a lot easier to fix than these other issues.
265.
by creata 1y ago
As far as I know, the main differences (in the body text) between LaTeX and, say, Word, are the linebreaking algorithm (Knuth-Plass, which is used for both ragged-right and justified text) and the microtypography package. Is there anything
266.
by creata 1y ago
True! But pjmlp was referring specifically to advanced JIT implementations, so I wondered which JITs he was referring to as advanced.
267.
by creata 1y ago
Thanks, that's an important point. Potentially never being able to move on from what you said or how it was perceived is a big difference.
268.
by creata 1y ago
Giving the blood type of the character is common in anime and manga. Wikipedia links it to a belief that blood type can predict personality. https://en.wikipedia.org/wiki/Blood_type_personality_theory
269.
by creata 1y ago
"RTFM" could excuse literally any syntax decision in any language. The hostility in your response to "lazy or stupid" devs is really funny given what a bad response it is.
270.
by creata 1y ago
Yeah, I know, I know. But I imagine many people would mentally want to bracket [e for x in xs for y in ys] like [(e for x in xs) for y in ys] and thus conclude that y is the outer loop.

More ›