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…
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…
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.
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…
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…
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…
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…
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…
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…
I mostly agree but there is a small effect: "Claims spectacular proofs with flawed arguments" might still be reason to doubt his future proofs more until verified. And mathematicians do use such criterions before…
That's only obvious in a vacuous sense. As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians:…
> So, we have numerous secure and high-uptime systems deployed whose methods were published even if source wasn't. He or others can always build on these if they want to replicate the results. I know that's technically…
Is there some website with some more info to read, for all those like me who dislike videos? I already googled "reflex facebook programming language" and found very little. Quoting the talk abstract…
Knowing assembly won't teach you the difference between legal overflows and ones triggering undefined behavior, or why you might need -fno-strict-aliasing to cast your pointers, and many more things. Does anybody know…
Many app stores (even for smartphone) have sandboxes where you can grant additional privileges. Of course the user (who else) has to decide whether they trust the app or not. But I'd be happier trusting a sandboxed…
Are you the OP author, or working on Pyston? I have basically two questions/curiosities — I'm not asking adversarially: 1) For which code is the C runtime most expensive? Typical Python code tries to leave heavy-lifting…
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…
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…
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.
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…
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…
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…
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…
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…
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…
I mostly agree but there is a small effect: "Claims spectacular proofs with flawed arguments" might still be reason to doubt his future proofs more until verified. And mathematicians do use such criterions before…
That's only obvious in a vacuous sense. As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians:…
> So, we have numerous secure and high-uptime systems deployed whose methods were published even if source wasn't. He or others can always build on these if they want to replicate the results. I know that's technically…
Is there some website with some more info to read, for all those like me who dislike videos? I already googled "reflex facebook programming language" and found very little. Quoting the talk abstract…
Knowing assembly won't teach you the difference between legal overflows and ones triggering undefined behavior, or why you might need -fno-strict-aliasing to cast your pointers, and many more things. Does anybody know…
Many app stores (even for smartphone) have sandboxes where you can grant additional privileges. Of course the user (who else) has to decide whether they trust the app or not. But I'd be happier trusting a sandboxed…
Are you the OP author, or working on Pyston? I have basically two questions/curiosities — I'm not asking adversarially: 1) For which code is the C runtime most expensive? Typical Python code tries to leave heavy-lifting…