c-cube

8 ms·

61.
by c-cube 3y ago
I also still don't get it, years later. I wrote a short post on this (a bit too inflammatory, tbh, sorry for the URL): https://blag.cedeela.fr/curry-howard-scam/ . A lot of logic and theorem proving can be done wi
62.
by c-cube 3y ago
You're funny. Exceeding in importance the Internet itself? That's an incredible amount of hype. Would you rather have chatGPT dialed by SMS in a world without Internet, or Internet without chatGPT? I know which one I'd choose
63.
by c-cube 3y ago
You can configure tokio with feature flags in cargo. I'm particular you can pick a single threaded scheduler.
64.
by c-cube 3y ago
Why would anyone use it for serialization, when json exists? Yaml is harder to parse and the implementations have a history of security issues because it's so complicated. If you're not writing it by hand why bother at all?
65.
by c-cube 3y ago
> you couldn't and it wasn't What are you talking about, millions of people do it and live without cars in cities. I did it for years in Paris and it's not a "smaller life" — the main things that are smaller are
66.
by c-cube 3y ago
That's called source available, not open source.
67.
by c-cube 3y ago
They say "major brands". Isn't porsche a luxury brand with relatively low sales in comparison to the big ones? As such it's not relevant to most consumers.
68.
by c-cube 3y ago
There's a workshop exploring that: http://www.sc-square.org/CSA/welcome.html . They're trying to bridge cas and smt.
69.
by c-cube 3y ago
Do you have any evidence for that? My impression is that Mathematica is built on a rewriting language along with thousands of built-in procedures (some of which are sat/smt). I don't think its core engine itself is smt.
70.
by c-cube 3y ago
In 2008 at univ I had a few classes using http://krakatoa.lri.fr/ . Tools definitely exist, although you could probably argue that the production ready version of that that people use in practice is really Ada/SPARK (bu
71.
by c-cube 3y ago
Isabelle is good at counter examples in ways few other proof assistants are. In general its automation is excellent, partly because it uses a less powerful logic (HOL instead of CIC; more expressive logics are harder to write automation for
72.
by c-cube 3y ago
That's called renting, not buying. There's no buyer in that case. And that's exactly the rent-seeking trend I talk about. Most virtual "purchases" are actually just rent because you don't actually own the thing
73.
by c-cube 3y ago
Rights to impose your will about something, should end at the point where you sell this thing to someone else. That's how it should be. Sadly a lot of companies are trying to rent rather than sell (see: ebooks, anything as a service, e
74.
by c-cube 3y ago
Thank you ^_^
75.
by c-cube 3y ago
They maintain a bunch of protobuf files, which is somewhat better and more efficient. You can still use json if you want.
76.
by c-cube 3y ago
Parkmobile sells your personal data, and pretty hard too. The email I gave them receives a metric ton of spam. It's infuriating.
77.
by c-cube 3y ago
> post one Abseil or folly both have optimized hashtables, I believe. Rust's standard HashMap follows the same design. It involves SIMD to look for a bucket whose hash matches the query's so redoing it in C every time you need
78.
by c-cube 3y ago
What does "my own interests" mean to chat GPT? It doesn't even have continuous existence, it exists only in a query/reply fashion. It doesn't have memory, a body to identify with, emotions, goals, fears, desires, or
79.
by c-cube 3y ago
When I looked at it a few years ago, the compiler didn't prevent you from accessing fields from the wrong variant, and didn't provide exhaustivity checks. So I think it still falls short of this (excellent) litmus test :/
80.
by c-cube 3y ago
I stopped being engaged when the author uses "normalcattle" in a unironic, disdainful tone. Then later on there's praise of RMS. I like the overall message, as a long time daily IRC user, but the contempt seeping from the who
81.
by c-cube 3y ago
Why don't you compare JSON + gzip to msgpack + gzip? That'd be a more fair comparison.
82.
by c-cube 3y ago
No need to prove! Any well calibrated bullshit detector should ring at 110dB when applied to claims mixing AI and quantum computing. (that said, "may eventually be possible" is so weak a claim it's already meaningless. Quantu
83.
by c-cube 3y ago
I don't think there's encoding overhead. It's like http, like you said, but just like http body encoding it seems that actual payloads are preceded with their length so that you just read n followed by n bytes. Look at the do
84.
by c-cube 3y ago
Unlike Larry Ellison, Zuckerberg, or Dick Cheney, he tweets often, loudly, and enjoys edgy memes and direct confrontations. I think that's also why he's attracting so much flak: he's actively looking for it.
85.
by c-cube 3y ago
It's payback from years and years of idolizing the man and how big a genius he's been for single handedly designing all these rockets and cars. Now it's become acceptable to criticize him, at a time where he's also publi
86.
by c-cube 3y ago
It still doesn't have sum types. Maybe 10 more years and Go can catch up to SML (a language from the 1970s). That's a big weakness for a static language this millennium.
87.
by c-cube 3y ago
I haven't tried but I'm curious about them: would a foldable (e)bike do it for you? You just don't leave it outside at all! I've been eyeing the Bromptons but without a commute it's harder for me to justify the cost
88.
by c-cube 3y ago
But then you make built-in types special. One of the tenets of C++ is that user defined types have as much power as built-in types.
89.
by c-cube 3y ago
CPU stuff, let's see... For a dev, maybe running their own program, compilers (sometimes with a lot of optimization passes), interpreters for python/ruby, an IDE with indexing over the whole project, running the OS itself, tests,
90.
by c-cube 3y ago
Yeah right, it can answer written form exams that are similar to previous ones, and are expressed in formulaic ways. That's impressive, don't get me wrong, but it's also already clear that ChatGPT makes for a terrible lawyer

More ›