pron

24 ms·

301.
by pron 6mo ago
Turns out it's not infinitely spawnable after all.
302.
by pron 6mo ago
> It's not that the benchmarks game is not a good benchmark suite, it isn't a benchmark suite. OK, but I was responding to someone who did consider it to be a benchmark suite. As long as we agree it's not a good benchmark
303.
by pron 6mo ago
First, your code is about having unsigned types represent the notion of non-negative values, but this is not the intent of unsigned types in C/C++. They represent modular arithmetic types. Second, it's not as simple as you prese
304.
by pron 6mo ago
I think all the unsigned arithmetic you need is already offered. Unsigned shift right is an operator; the primitive wrappers offer compareUnsigned, divideUnsigned, and remainderUnsigned, as well as conversion methods; unsigned exponentiatio
305.
by pron 6mo ago
> That's true for signed numbers too though? `int_min - 2 > int_min` As someone else already pointed out, that's undefined behaviour in C and C++ (in Java they wrap), but the more important point is that the vast majority of
306.
by pron 6mo ago
> But I would say if you know a value will logically always be >= 0, better to have a type that reflects that. Except that's not quite what unsigned types do. They are not (just) numbers that will always be >= 0, but numbers w
307.
by pron 6mo ago
In Java, unsigned arithmetic is available through an API and, as you said, it is pretty much only needed when marshalling to certain wire protocols or for FFI. Built-in unsigned types are useful primarily for bitfields or similar tiny types
308.
by pron 6mo ago
I don't understand what you're trying to say. I said that the Benchmark Game is not a good benchmark suite in the sense that it does not measure language speed differences since 1. it compares different algorithms, and 2. it doesn
309.
by pron 6mo ago
> Should Curl have a slower startup time? Probably not. Of course, but I don't think anyone would consider curl to be of little consequence. There are many small programs that are very important, but in general more value is in la
310.
by pron 6mo ago
> And makes no claim to be. I know. I don't understand why you think I have a problem with the site's honesty. It's a poor benchmark suite, and it admits it is. We're in agreement. > Here's something that coul
311.
by pron 6mo ago
All benchmarks tell the truth about themselves. That has never been what makes benchmarks good or bad. The worst and best benchmarks ever made are both truthful about their results. But a good benchmark suite is one that covers a variety of
312.
by pron 6mo ago
> If it evolves. My inexperience with apps that large is spread across dozens of businesses that are 20+ years old. 1M LOC is not a required thing. Just to be clear, the cost of maintaining a program in a low-level language is always h
313.
by pron 6mo ago
The problem with benchmarks isn't that they themselves are lying. Benchmarks always tell the truth - about themselves. The problem is in the conclusions people draw from them. In the nineties benchmarks were still a little extrapolatab
314.
by pron 6mo ago
> The fallacy in that reasoning is that a program that's using a lot of CPU (especially if it's a huge MLOC-sized app) is most likely using up its CPU on memory throughput, not pure number-crunching compute! No, there's no
315.
by pron 6mo ago
> JavaOne long ago, there would be mixed messages I didn't say that short-running benchmarks don't measure anything interesting, only that they don't say much about long running programs, where the same mechanisms can exhi
316.
by pron 6mo ago
I feel like this has been a great discussion but all the good technical talk is tapering off. There's more rhetorical semantics now than anything. But I appreciate you teaching me. I'm a bit tired in this reply. I wish I could fin
317.
by pron 6mo ago
Not only is it easy, the ability to extend the computable into the non-computable is quite convenient. For example, computable numbers can be directly treated as a subset of the reals. This is exactly how TLA+ works: https://pron
318.
by pron 6mo ago
That's not true. Non-constructive logics are extensions of constructive logics. You can express any algorithm in TLA+, and much more than algorithms. You are right that when using non constructive logics, it's not guaranteed tha
319.
by pron 6mo ago
> In the case of Rust, it has Arenas, stack allocated structs, and generics via monomorphization. Not only can you avoid both of these things, it doesn't even seem that difficult. If you're saying the borrowchecker just becomes
320.
by pron 6mo ago
> in surfacing computational content, which is the whole point of constructive proof The point of a constructive proof is that the proof itself is in some way computational [1], not that the algorithm is. When I wrote formal proofs, I
321.
by pron 6mo ago
Oh, if you mean that most algorithm correctness proofs are finitary and therefore don't need to explicitly rely on the excluded middle, that may well be the case, but they certainly don't try to avoid it either. Look at any algori
322.
by pron 6mo ago
Oh, so I have used formal methods for many years (and have written about them [1]), including proof assistants, and have never found that constructive logic in general and type theory in particular makes proofs of program correctness any ea
323.
by pron 6mo ago
> However long (programs run) they never seem to become "long-running". Most application servers are expected to run without issue for at least a day. Our acceptance tests run high workloads for 1, 7, and 30 days. The longest r
324.
by pron 6mo ago
... and also to classical logic. Liveness proofs typically require finding a variant that converges to some terminal value, and that's just as easy to do in classical logic as in constructive logic. I've been using formal methods
325.
by pron 6mo ago
The Turing test pits a human against a machine, each trying to convince a human questioner that the other is the machine. If the machine knows how humans generally behave, for a proper test, the human contestant should know how the machine
326.
by pron 6mo ago
How have you used the Curry Howard correspondence to make proving the correctness of non-trivial algorithms easier (than, say, Isabelle/HOL or TLA+ proofs)?
327.
by pron 6mo ago
> Obviously, we want to stick with useful data structures, so we use constructive logic for programming. I don't know who "we" are, but most proofs of algorithm correctness use classical logic. Also, there's nothing &
328.
by pron 6mo ago
> That being said, I am not understanding this narrative that low level projects, as they grow, always devolve into an inefficient dynamic soup. The Linux kernel is millions of lines and uses function pointers sparingly and deliberately.
329.
by pron 6mo ago
First, confusing feminism with femininity or, conversely, patriarchy with masculinity is such a basic error - and not one of nuance - that shows at least an intentional disinterest. There is no "goal to decouple", because if an id
330.
by pron 6mo ago
Governments have long funded artistic projects. I'm sure some people oppose government funding for the arts, but there's nothing unusual about it. Obviously, not all artists get government funding, but such funding is an establish

More ›