IsTom

> 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 when this kind of loop is generated by macros/templates in some unreachable case left after const folding.

> 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 language. There's also languages like idris2 and f-star, but they don't seem to have much traction.

`find` does a lot more things than that.

It's also a particle and a self-propelled gun. There's a limited number of short legible words.

Why'd 800x600 be this popular? Is this some specific device? Is this 90s? Seems suspicious to me.

> 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 "summer tyres get too hard in the cold" idea could very well come from places where the typical winter is at least < -5°C. It's not uncommon in central/eastern/northern europe for temperatures to be < -10°C for extended periods of time.

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 not below 0°C? That sounds like "winter tires are worse than all-seasons tires in winter if you exclude winter".

Yes, but typically people are not doing this on every command and if you're globbing files it'll get used as flag.

> anything but NUL is valid.

And slash/!

If they reject more ads they get less money.

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 know which states are reachable and which are not? That takes time.

It only takes a botched condition here (forgot a "not"? swapped "and"/"or"?), a swapped variable name there, code that looks ok, but isn't.

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

To be a slightly more neutral It'd be a nice opportunity to base it on esperanto.

Pretty cool, especially in finite fields. Though coefficients seem to blow up pretty quick in Q?

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 people die. And then the remaining people will have trouble keeping that level of technology with how sudden the change would be.

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 it leaves a lot of space for specification bugs.

And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.

> To meet and spend time with other human beings.

The design is very human.

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 done.

From outside of US this seems extremely ass backwards.

On the other hand it means that states can just not do that and leave their citizens without clean drinking water.

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 going against the general consensus you should present something more than nebulous assertions that it's wrong.

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.

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 operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.

> 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...

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?

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 and after adjustment will get some new interesting events, but still actually processing the candidates might take a long time.

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 trying to make mac/ios apps.

If 30-40k timelines are right that's way before agriculture and any kind of "economy". It's firmly hunter-gatherers and there's not much of that to do when it's after sunset.

I can imagine them not having a lot to do during winter nights, besides sitting by the fire. That's a lot of time for carving.

I think the core of this is google vs oracle case. I think they'll be in the clear unless they hit some specific (design?) patents.

I've used docker until recently just because it was what I was used to. It turned out I can basically just `apt install podman` and it'll just work. I might have stayed a bit behind the times with having podman slotted as a redhat thing.