unexpectedtrap

7 ms·

1.
by unexpectedtrap 8d ago
That’s just the aberration, no? I.e., you can simply smash A and observe some rotation. Since there are no non-collinear accelerations in this case, it’s certainly not the required effect (which is called Wigner rotation). In the sources I
2.
by unexpectedtrap 27d ago
Plan 9 is essentially exactly that, which clearly was inspired by the Oberon’s GUI. By the way, does then Emacs count as such? Or maybe you should take a look at Genera, however, I’ve never really tried it. Also the original Metro design as
3.
by unexpectedtrap 2mo ago
Using LLMs to generate piles of code and/or proofs of dubious quality is very questionable thing, and I understand these non-stop debates about it. But in this case, as using plain brute force is already quite a common thing in searchi
4.
by unexpectedtrap 5mo ago
>I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it? The reason is to be able to write mathematical proofs, including proofs about your code, but not to attac
5.
by unexpectedtrap 5mo ago
>It definitely is a bad convention because it's highly surprising. You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising a
6.
by unexpectedtrap 5mo ago
No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel , this part of a codebase has hardly changed since Lean 3). Almost all
7.
by unexpectedtrap 5mo ago
Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that
8.
by unexpectedtrap 5mo ago
Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not
9.
by unexpectedtrap 7mo ago
Glad to see Rust project under AGPL-3.0. I wish to see more Rust projects under (A)GPL, because (A)GPL is rare in the Rust community for some reason.
10.
by unexpectedtrap 7mo ago
So instead of using programming languages designed specifically to effectively express algorithms and data structures, we are going to use natural language like English that is clearly not expressive enough for this? It’s like rewriting a p
11.
by unexpectedtrap 8mo ago
I saw this DSL on HN yesterday, and this syntax is total garbage. It’s some stupid mixture of different PLs. Are you seriously OK with this so that you keep posting it here? I don’t even want to look through source code knowing what garbage
12.
by unexpectedtrap 8mo ago
It’s funny to see that even nowadays just a few people understand Windows 8’s UI, while the majority in these comments just blindly shits at it. Not surprising, though, since there are so many happy users of crap UI’s like KDE around. Sadly
13.
by unexpectedtrap 10mo ago
They now provide at least somehow working x86_64 images. It’s of course funny for a project started in the 90s to get x86_64 support only in the 2020s, but it’s still progress in relative terms.
14.
by unexpectedtrap 10mo ago
No, it’s just you having some strange prejudices about these words (probably driven by blind faith in some overhyped technologies), so go better overregulate your preferred echo chamber.
15.
by unexpectedtrap 10mo ago
I feel the same, because it seems that the only desktop-ready OS under GPL today is GNU/Linux, and it feels too bloated nowadays (not to mention that Linux is effectively stuck under GPLv2). Something like FreeBSD feels much lighter an
16.
by unexpectedtrap 10mo ago
IANAL, but you can’t actually just relicense code, even if it’s under BSD‐like license. What you can do is to release this code in the binary form without providing the source code.
17.
by unexpectedtrap 1y ago
Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.
18.
by unexpectedtrap 1y ago
Euclid’s Elements “rigorous proof” is not the same thing as the modern rigorous proof at all. >But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis. This doesn’t mean that these i
19.
by unexpectedtrap 1y ago
“Paraconsistent logic” or “paraconsistent set theory” is what you are searching for.
20.
9aout: Native Plan 9 binaries on Linux(github.com)
3 points by unexpectedtrap 3y ago|0 comments