IsTom

7 ms·

1.
by IsTom 8d ago
Yeah, and it's alt+k on my default keyboard layout on debian… I think some punctuation is available on macos as well — so perhaps it's a windows-ism that «only AI can use punctuation».
2.
by IsTom 8d ago
> The "trick" is that they are not Turing-complete, they mandate termination of every expression. I don't think this is a big deal for day-to-day programming. You're trying to stay in n, nlogn or maybe n^2 realm most
3.
by IsTom 8d ago
Even more concretely, the halting problem for turing machines with halting problem oracle would be undecidable for them. And if you could solve that you won't believe what problem would be undecidable. It's turtles all the way up.
4.
by IsTom 8d ago
Yeah, but then you need compiler to somehow know if it's truly unreachable to know when to emit the warning and when to not do that.
5.
by IsTom 8d ago
> should've explored a rule that required the compiler to emit a diagnostic or error for trivial loops (whether as defined by C11 or otherwise), requiring the programmer to explicitly insert ::yield or similar It wouldn't work
6.
by IsTom 8d ago
> no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove Lean can be used as a regular programming langua
7.
by IsTom 10d ago
`find` does a lot more things than that.
8.
by IsTom 12d ago
It's also a particle and a self-propelled gun. There's a limited number of short legible words.
9.
by IsTom 12d ago
Why'd 800x600 be this popular? Is this some specific device? Is this 90s? Seems suspicious to me.
10.
by IsTom 12d ago
> but I guess you get into problems with it being ice and snow that you're testing If it's not actively snowing for a few days roads get clear by thawing during day because of salt/cars being hot/sun shining. The &quo
11.
by IsTom 13d ago
I'm a little bit confused about these tire claims as > down to 0C / 32 F (he didn't test colder conditions) I get that people live in different places, but that's a huge caveat. How's that winter if you're n
12.
by IsTom 13d ago
Yes, but typically people are not doing this on every command and if you're globbing files it'll get used as flag.
13.
by IsTom 13d ago
> anything but NUL is valid. And slash/!
14.
by IsTom 13d ago
If they reject more ads they get less money.
15.
by IsTom 14d ago
For small separate changes in isolation then maybe it's ok? But not for whole days 8 hours each. But then you need to watch for bugs coming from interaction with previous changes and in 700k loc that might be nontrivial. How do you kno
16.
by IsTom 15d ago
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues/14576
17.
by IsTom 16d ago
To be a slightly more neutral It'd be a nice opportunity to base it on esperanto.
18.
by IsTom 17d ago
Pretty cool, especially in finite fields. Though coefficients seem to blow up pretty quick in Q?
19.
by IsTom 18d ago
Technology depends on a lot of people cooperating around the globe. Disrupt a few critical chains (power generation, fertilizers, computers), add a bit of good old war and you'll soon be in the era before Haber process and a lot of peo
20.
by IsTom 18d ago
I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with ergonomics, but
21.
by IsTom 19d ago
> To meet and spend time with other human beings. The design is very human.
22.
by IsTom 20d ago
Yes > Rather, the remedy for Plaintiffs’ injuries lies in pursuing tort claims, electing representatives who will better manage the public-water system, and petitioning their representatives for other remedies. which is easier said than
23.
by IsTom 21d ago
On the other hand it means that states can just not do that and leave their citizens without clean drinking water.
24.
by IsTom 21d ago
Per https://en.wikipedia.org/wiki/Peano_axioms#Set-theoretic_mod... > The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.[15] If you're g
25.
by IsTom 21d ago
You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
26.
by IsTom 22d ago
It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given. You don't need to add any axioms, you just build some sets to represent numbers and make
27.
by IsTom 22d ago
> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC. https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
28.
by IsTom 23d ago
Or you could wait a day or two to write about it, but with initial reactions etc. added. 24-hour new cycle came into view in 80s I think?
29.
by IsTom 24d ago
If this anything like CERN detectors, they get amounts of data so vast that they have to discard almost all of it to be even able to record it. Depending on heurestics you use to discard data you might be discarding what you are looking for
30.
by IsTom 25d ago
I still remember getting support mail every time Apple released an OS update. For a week or two there'd be reports of things crashing randomly with stacktraces that didn't seem to make much sense. One of reasons why I stopped tryi

More ›