> I have never run across anyone with legal training using "spirit" language. I know what you mean (and agree), but some spirit language seems required by the subject matter :-)...
Throwing away large chunks of code is what optimizers exist for! Sadly, most discussions of UB only show when it "goes wrong" (has surprising results), not when it goes right!
Do you have a link? That might mean a set of different things, ranging from very hard to impossible; strictly speaking, this seems to go against Godel's theorems tho there are standard workarounds. I'm familiar with…
@ceilingcorner's main point is that, no matter how healthy you live, an obese person is more likely to infect you. I don't know if I buy that, but I agree none of your answers seem to be on point.
AFAIK, Wikipedia's info on the Latin Modern regressions from Blue Sky is accurate. Neither version is the original CM font or has had as much fine-tuning put into it, but (EDIT) the Blue Sky version was at least worked…
Great example, can I please borrow that? Is a link sufficient attribution?
Should have been more careful — in C and C++ they were implementation-defined. But both theory and practice did not mandate a concrete model — GCC already violates that and implements a mishmash of PVI and PNVI. From…
Why don’t they just disable optimizations then? I think that’s because they also want performance, even when it requires pointers to not be just addresses. And pointers weren’t addresses before either. My favorite…
You forget that basically _all_ int<->ptr casts were undefined before and that compilers already violated the concrete semantics. But kudos for finding an official source of misinformation. What’s more, the committee…
But you can’t compare to the concrete model, because it’s not the status quo. That ship already sailed with C89 and strict aliasing. Ptr2int casts were never legal, and support was inconsistent. For instance, GCC…
First, this change is reducing undefined behavior* (EDIT: see below), and that undefined behavior (most casts between pointers and integers) did _not_ work reliably in practice. And in fact, the semantics they chose is…
> Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction. > After the re-naming they are never heard of again. Beyond all other…
Coq’s name _was_ meant to be offensive to English speakers. And the team does want to avoid names that are offensive in other languages, as EVERYBODY does when choosing international brand names.
We _know_ it doesn’t just come from Coquand’s name, because Gérard Huet very clearly said so.
The thread is full of stories like “woman says she works on Coq and gets harassed” or “woman foresees this problem and avoids learning Coq” or “Coq teacher (male or female) struggles to talk about Coq because students…
Knuth also uses assembly in his book on algorithms. But generally, algorithms researchers seem to not care about abstractions, as witnessed by TeX and LaTeX in multiple ways. That's probably because when you really need…
That sounds weird; all journals I know are paid either by readers or by the submitter (the latter is called gold open access).
"If it compiles it works" is just not true, just a very bad description for a true phenomenon. If there weren’t people repeating that seriously, you’d be attacking a strawman. People do say that, but that’s on those…
Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.
Having used both, Coq proof terms aren't Agda proof terms. Coq provides neither "real" dependent pattern matching nor edit-time tactics. Long-term, the vision in Agda would be to support metaprogramming closer to what…
> automatic memory management without the overhead of a garbage collector I’d also love magic, but you can’t just wish it into existence. That’s a hard problem that V doesn’t solve yet. One should be open minded, but…
Citation needed? I’m a postdoc, and that doesn’t ring remotely true. At least in CS, authors get most of the scientific credit all the time, and not just in citations to “FirstAuthorSurname et al.”, or in giving talks…
The title of Doctor witnesses that the owner advanced humanity’s knowledge, and often turned the impossible into possible (as here). It’s not “just” a degree. It’s also not inherited. That you compare work titles with…
Without knowing Oracle's approach, this sort of problem is no different from any other software, even tho it reaches a larger scale. Branch from master, and rerun tests before the final merge, like you should in any…
Scalac has evolved considerably, but it appears to be much harder to evolve. The Scalac team and contributors are backporting some of the Dotty features, but this is far from a trivial effort. Doing the same changes in…
> I have never run across anyone with legal training using "spirit" language. I know what you mean (and agree), but some spirit language seems required by the subject matter :-)...
Throwing away large chunks of code is what optimizers exist for! Sadly, most discussions of UB only show when it "goes wrong" (has surprising results), not when it goes right!
Do you have a link? That might mean a set of different things, ranging from very hard to impossible; strictly speaking, this seems to go against Godel's theorems tho there are standard workarounds. I'm familiar with…
@ceilingcorner's main point is that, no matter how healthy you live, an obese person is more likely to infect you. I don't know if I buy that, but I agree none of your answers seem to be on point.
AFAIK, Wikipedia's info on the Latin Modern regressions from Blue Sky is accurate. Neither version is the original CM font or has had as much fine-tuning put into it, but (EDIT) the Blue Sky version was at least worked…
Great example, can I please borrow that? Is a link sufficient attribution?
Should have been more careful — in C and C++ they were implementation-defined. But both theory and practice did not mandate a concrete model — GCC already violates that and implements a mishmash of PVI and PNVI. From…
Why don’t they just disable optimizations then? I think that’s because they also want performance, even when it requires pointers to not be just addresses. And pointers weren’t addresses before either. My favorite…
You forget that basically _all_ int<->ptr casts were undefined before and that compilers already violated the concrete semantics. But kudos for finding an official source of misinformation. What’s more, the committee…
But you can’t compare to the concrete model, because it’s not the status quo. That ship already sailed with C89 and strict aliasing. Ptr2int casts were never legal, and support was inconsistent. For instance, GCC…
First, this change is reducing undefined behavior* (EDIT: see below), and that undefined behavior (most casts between pointers and integers) did _not_ work reliably in practice. And in fact, the semantics they chose is…
> Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction. > After the re-naming they are never heard of again. Beyond all other…
Coq’s name _was_ meant to be offensive to English speakers. And the team does want to avoid names that are offensive in other languages, as EVERYBODY does when choosing international brand names.
We _know_ it doesn’t just come from Coquand’s name, because Gérard Huet very clearly said so.
The thread is full of stories like “woman says she works on Coq and gets harassed” or “woman foresees this problem and avoids learning Coq” or “Coq teacher (male or female) struggles to talk about Coq because students…
Knuth also uses assembly in his book on algorithms. But generally, algorithms researchers seem to not care about abstractions, as witnessed by TeX and LaTeX in multiple ways. That's probably because when you really need…
That sounds weird; all journals I know are paid either by readers or by the submitter (the latter is called gold open access).
"If it compiles it works" is just not true, just a very bad description for a true phenomenon. If there weren’t people repeating that seriously, you’d be attacking a strawman. People do say that, but that’s on those…
Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.
Having used both, Coq proof terms aren't Agda proof terms. Coq provides neither "real" dependent pattern matching nor edit-time tactics. Long-term, the vision in Agda would be to support metaprogramming closer to what…
> automatic memory management without the overhead of a garbage collector I’d also love magic, but you can’t just wish it into existence. That’s a hard problem that V doesn’t solve yet. One should be open minded, but…
Citation needed? I’m a postdoc, and that doesn’t ring remotely true. At least in CS, authors get most of the scientific credit all the time, and not just in citations to “FirstAuthorSurname et al.”, or in giving talks…
The title of Doctor witnesses that the owner advanced humanity’s knowledge, and often turned the impossible into possible (as here). It’s not “just” a degree. It’s also not inherited. That you compare work titles with…
Without knowing Oracle's approach, this sort of problem is no different from any other software, even tho it reaches a larger scale. Branch from master, and rerun tests before the final merge, like you should in any…
Scalac has evolved considerably, but it appears to be much harder to evolve. The Scalac team and contributors are backporting some of the Dotty features, but this is far from a trivial effort. Doing the same changes in…