Blaisorblade0

5 ms·

1.
by Blaisorblade0 5y ago
> 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 :-)...
2.
by Blaisorblade0 5y ago
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!
3.
by Blaisorblade0 5y ago
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 https:/&
4.
by Blaisorblade0 5y ago
@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.
5.
by Blaisorblade0 5y ago
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 on by paid profe
6.
by Blaisorblade0 5y ago
Great example, can I please borrow that? Is a link sufficient attribution?
7.
by Blaisorblade0 5y ago
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 N2176, Sec. 6.3.2.3, p.
8.
by Blaisorblade0 5y ago
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 example of “pointers are
9.
by Blaisorblade0 5y ago
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 already gave
10.
by Blaisorblade0 5y ago
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 sometimes tracks pointer pr
11.
by Blaisorblade0 5y ago
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 rather sensible. But
12.
by Blaisorblade0 5y ago
> 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 corrections, the peop
13.
by Blaisorblade0 5y ago
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.
14.
by Blaisorblade0 5y ago
We _know_ it doesn’t just come from Coquand’s name, because Gérard Huet very clearly said so.
15.
by Blaisorblade0 5y ago
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 are uncomfortable”. Yo
16.
by Blaisorblade0 7y ago
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 to invent a fa
17.
by Blaisorblade0 7y ago
That sounds weird; all journals I know are paid either by readers or by the submitter (the latter is called gold open access).
18.
by Blaisorblade0 7y ago
"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 people, not Ru
19.
by Blaisorblade0 7y ago
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.
20.
by Blaisorblade0 7y ago
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 you do
21.
by Blaisorblade0 7y ago
> 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 what’s the eviden
22.
by Blaisorblade0 7y ago
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 about the work (especi
23.
by Blaisorblade0 7y ago
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 that suggests you have
24.
by Blaisorblade0 8y ago
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 other software? (Ma
25.
by Blaisorblade0 8y ago
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 Dotty is typically mu
26.
by Blaisorblade0 9y ago
Verification of unsafe languages such as unsafe Rust (here), or C, PHP or assembly (in other research) tries to show if some particular program is correct or not — by exhibiting bugs, proving safety, or both. Tons of approaches exist. But v
27.
by Blaisorblade0 9y ago
Rust can be criticized ( https://news.ycombinator.com/item?id=16305437 ), but flaws will be spotted. I’ll concede nonsense on other topics might have more leeway.
28.
by Blaisorblade0 9y ago
This is one research grant on Rust among tons of grants on other projects. And it funds research . When somebody has equally valid research project on C, rest assured it’ll be funded as well, as it has already happened (EDIT) with resear
29.
by Blaisorblade0 9y ago
But you are aware real-world compilers are exploiting more and more UB and keep breaking existing software? Maybe you are, but the comment does not seem to reflect that. Either way: The good thing is, after compiler writers start exploiting
30.
by Blaisorblade0 9y ago
Because (I'd guess, as a PhD student in another CS field) any advisor worth its salt would advise a grad student to work on something else first, get tenure, and then maybe approach this problem. Until yesterday, most researchers agree

More ›