Viewing profile — Blaisorblade0

> 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 stan…

@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…

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) th…

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 impleme…

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 add…

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 misinfor…

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…

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

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

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 internation…

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) struggl…

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'…

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

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 s…

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

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 “FirstAuth…

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 inherit…

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 …

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 tri…