What would be your goto for the ML training pipeline?
I have the impression that Python basically wins by default in those spaces due to the lack of many good libraries in other languages (except for, like, C++).
But curious if this is just a very outdated view of the world
While PG's behavior doesn't guarantee a lack of data corruption, "an extension crashed, all bets are off, tear everything down" is going to give you a much better fighting chance against data corruption vs the alternative.
Not to minimise compcert's work nor to trivialise the equivalent kind of work in Rust but I wonder how much of the Compcert difficulty on dead code elimination is downstream of C semantic futziness. I know that CompCert has a whole notion of external visibility that it has to deal with that I _think_ would be way more straightforward in Rust.
My experience writing Roq (very limited!!!) is that it also lends towards kinda brute forcing your way through something. If you have your set of proof lemmas and you tie it all together there's not that much incentive to simplify the proofs (that are irrelevant anyways, according to the theories). So the 1200 LoC might be "oh we could have maybe done this in 400 with more thinking but ... well... this is working yeah?"
trying not to trivialize it all. Just kinda hoping that we do have a more provable future ahead of us, and that CompCert represents (hopefully) an upper bound of difficulty just due to the nature of the source language.
> The issue was labeled p-critical and i-miscompile, out of +61K rust issues there only 7 (including this one) that are both p-critical and i-miscompile, to me those are the most dangerous kind of bugs a compiler can have, given that they violate the contract between the programmer and the language. They show that not every safe code you write is safe. And also more generally there are only 247 p-critical issues to begin with.
I don't mean this in a snarky way or the like... and I guess the fact there are so few of these are a good indicator that the current processes are working decently well... but I would be very curious on a post-mortem from maintainers on how this bug got through. Miscompiles feel like the scariest sort of thing.
Maybe the deep and dark secret is simply that compiler optimizations are just extremely prone to mistakes and we all are just lucky enough that most messed up optimizations will break _something somewhere_ early enough to not get merged.
I really wonder what "randomixed testing" looks like in practice. What is the measure of success/failure?
I undrestand for fuzzing you have a very basic "doesn't crash" metric. Property based tests.... you gotta write properties for the PBTs to work on. What is the randomized testing hitting?
There’s s fun subgenre of blog titles in Japanese like なんとか作ってみた／やってみた. Like “we tried something”/“we did something” etc
A great sort of tone setter title format. Basically you know you’re about to just read someone talk about their experience in a casual way. Feel like everyone should try writing blog post titles like that
“I installed Arch Linux on my toaster” “I dug a whole in my back yard” “We made a very big paper airplane” is going to lead to very interesting blog post vibes
I had to do "write code on paper" stuff as part of french engineering school entrance exams.
It's fine (tho annoying when you lose points to "typos"), but it limits what kinds of problems you can reasonably put on the exam. You'll definitely lean a bit more into theoretical stuff than practicals. Which is fine for some courses, I think a bit less interesting in other courses.
Remember, the hand written code is also harder for reviewers to grade! You have to manually run the code in your head, for example
Having said all that... "we've booked the computer room, you don't have internet, go type up all your stuff in this VM we have set up" feels fine if you don't like this constraint IMO
Is this true even for more targeted prompts that aren't about looking over an entire codebase or w/e? I just stick to my sub pricing and find good success on targeted requests, but I wonder if I would run up against things even then if not for subsidies.
the justification given for the ban (provided in other sources) is that Polestar's software stack is made in China. The theoretical spooky thing is China forcing some "evil" software update that stops all the Polestars.
The Volvo distinction is ... I mean maybe the Volvo software stack is in Europe or the US. Maybe it's also in China!
I do not really subscribe to this philosophy but what's going on isn't a "Polestar would be tar riffed" thing. It's an outright "you can't sell em" thing
Emacs in particular I suffer so much from basically guessing what needs to be escaped or not. I know `rx` exists[0] as an alternative but it's not really fun to use.
Even beyond the regex syntax itself, you often also start running into encoding problems when trying to actually use them. Typing the regex in a shell? Make sure to esacpe stuff properly. Regex in Python? Make sure it's a raw string. Etc etc etc
It's a modern miracle we're at least within rhyming distance of how to write regexes in most tools.
I've had this idea of building a codec that would similarly overfit to specific images. But the codec itself would not be a fixed size transformer... instead you could just mess around with the sizing to get better quality/smaller size.
So the codec would be something like:
<header describing image size + transformer layer shape>
<transformer data itself>
I've seen experiments where people have a "fixed" pipeline but I think having something more dynamic would work quite well.
I think if you believe that the aids types give for refactoring are equivalent to structural editing, then you are the one who might not get the value of typing information (I say this as a Python person, and am totally willing to accept lack of typing info in plenty of situations)
REPLs are nice and good, but when you're working on large enough systems it's nice to have some static foundations for your facts.
> There’s no “defederation” because there’s no analog of “community instances” that may fight with each other.
If Bluesky specifically wanted to just not have its user interact with some other entity in ATProto-land would they be able to?
My impression is that the answer to this is "yes", because people are signing up to Bluesky and relying on Bluesky to hold on to their posts etc.
Similar to how Email is all federated but in practice a bunch of people use email from one of a handful of large service providers who (in practice, not necessarily for nefarious reasons) do end up blacklisting certain email senders.
The RSS-reader example feels a bit different on the ground because for a given user, "store a list of websites you care about" is not a complicated endeavor.
For the "short-form social media with algorithmic timeline" usecase (which isn't all atproto is about, granted!) "users self-host a thing to scoop up enough of the world's posts to then make a local algorithmic timeline" doesn't... doesn't feel very feasible, right?
I guess the blogspot comparison is apt... but if "full" self-hosting requires a relay with quite some juice ($30 is "cheap" but... compared to a pile of files to host your own blog...), then in practice we're going to see a heavy amount of centralization anyways right?
as someone who deals with dep upgrades and forensics when trying to figure out a bug I would get _so mad_ if `git diff` didn't show the diffs to lock files.
I get what you're saying about it being line noise but when you need it you need it!
> I see absolutely zero value in something like Fin.
Y'all really over indexing on the "AI"-ness of intercom. Intercom is a chat box and help pages. Those are nice to have and nice to not have to build yourself (you can build your own help pages... great, now you're managing content and have to have an admin to update the docs etc!)
People here really forgetting the notion of "core competency".
"This user is contacting us, and has previously contacted us about something, and we want records of this" is a basic need.
> We replaced our helpdesk with Hermes
You didn't just put a computer somewhere and have a customer go up and type on the computer right? You have surrounding infrastructure on that right? That is the value add.
the Gameboy, not the SNES, but this talk is very very good at going in detail about a bunch of internals. The graphics stuff is 29 minutes in but I love the whole video. Very much a high level guide to building a "retro-y" fantasy console for people into that stuff
blog: https://rtpg.co