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