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 standard workarounds.

I'm familiar with https://coq.discourse.group/t/alpha-announcement-coq-is-a-le..., which was just hard, but it does not prove Lean consistent, it only lets Coq process the Lean stdlib.

@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 on by paid professionals.

https://en.wikipedia.org/wiki/Computer_Modern#Latin_Modern

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 N2176, Sec. 6.3.2.3, p. 5-6: > An integer may be converted to any pointer type. Except as previously specified, the result is implementation-defined, might not be correctly aligned, might not point to an entity of the referenced type, and might be a trap representation.

> Any pointer type may be converted to an integer type. Except as previously specified, the result is implementation-defined. If the result cannot be represented in the integer type, the behavior is undefined. The result need not be in the range of values of any integer type.

AFAICT, that doesn’t even guarantee that a roundtrip is the identity — which C++ mandates and is still the case: http://eel.is/c++draft/expr.reinterpret.cast#5

EDIT: GCC does have those restrictions in place already: https://gcc.gnu.org/onlinedocs/gcc-11.1.0/gcc/Arrays-and-poi...

and since a while (earliest relevant docs I could find easily): https://gcc.gnu.org/onlinedocs/gcc-3.1.1/gcc/Arrays-and-poin...

EDIT2: LLVM doesn’t document this “implementation-defined behavior” (or most others), even if docs are explicitly required by the standard; but it does use pointer provenance in practice already, but not in a way that’s easy to explain.

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 aren’t addresses” is this kind of code:

int a[…]; int b[…]; /* … */ a[i] = 0; b[j] = 1; return a[i];

Ignoring this discussion for a moment, wouldn’t you expect `return a[i];` to optimize to `return 0;` here? After all, `a` and `b` are disjoint arrays! I’m sure many would be disappointed if the compiler did not do that optimization, right?

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 license to implementations to be “overzealous”, as you call them. That did contradict the standard, but they never bothered to fix it.

So it’s not the first time the C committee contradicts itself and doesn’t bother to resolve the contradiction. So yes, you’re entitled to feel you’ve been lied to before, they’re just being honest now.

GCC has been using http://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm to justify its use of provenance, even when it contradicts the standard.

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 provenance through integers; this proposed change will make that clearly illegal.

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 yes, some code with UB which works for now might break. But that’s true whenever you upgrade your C compiler or use optimizations, so for correctness you shouldn’t do either! People working on certified embedded software have known that for long.

The real problem is that C users have been lied to. They’ve been taught the lie that C pointers are just addresses, that memory is an array of bytes, that relying on this lie is robust, and that this combination is fast. But this combination is impossible.

EDIT: officially some behavior was implementation-defined, but implementations made it undefined anyway — either officially or via bugs; links in subthread.

> 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 people complaining here are professional Coq users of both genders.

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 are uncomfortable”.

You seem to suggest those people train everybody around them to change behavior.

Meanwhile, every company picking a brand name will do the smart thing and avoid anything ridiculous in any of their target market; yet somehow if this happens in public it’s a scandal.

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 fancy algorithm (which is their job), that will often not be built out of reusable components.

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 people, not Rust.

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 you do in FP languages. But even now, there are domains where Agda is competitive (tho they seem to be in mechanizing mathematical theories, as in, things designed by mathematicians to be compact). To prove software correct, you'll likely end up with with proofs you'll want to automate.

Regarding compatibility: neither Coq nor Agda used to have much of it; nowadays Coq is maintained together with a large set of community projects, and code is much more stable. Still tons to do.

> 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 evidence V can solve this? TLDR: not very compelling; just examples of existing techniques, and wild promises.

What docs show(fn1), and doesn’t even work according to reports, is an easy example of an existing technique — escape analysis, something that JVMs implement. It’s also hard enough to do properly, and it’s taken pretty long for HotSpot to handle some trickier cases. I also wonder how you’d implement the hard cases without an AST. And there’s no citation to the scientific literature, so you could fear the author just figured the basic idea, and thought the rest was easy. But escape analysis can’t handle everything, so usually you need a GC. Nobody knows how to avoid that, a solution would be novel research. So, what does V bring to the table?

> For more complex cases manual memory management is required. This will be fixed soon.

Ah, so you’ll just “fix soon” an open research problem? Wow. Not very compelling. Also:

> V will detect memory leaks at runtime and report them.

But... if you could avoid manual management, wouldn’t leak be impossible? So why would you do both? Unless you want to report the leaks that automated memory management doesn’t fix — memory that is reachable but never going to be used. But never seen anything good at detecting those leaks.

Also, wouldn’t you you need (an optional) GC or refcounting to do even that basic reporting? Sure you can, but doesn’t that add to the implementation complexity?

fn1: https://vlang.io/docs#memory

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 (especially in CS). They’re the ones doing most of the hard work and thinking.

Advisors often range from consultants/consulents to managers. Not because they’re not smart, but because they seldom have months of uninterrupted time to focus on a problem intensely enough.

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 no idea on what you’re talking about.

One can make intelligent arguments about the use of such titles. These aren’t.

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? (Many processes fail that criterion, see https://bors.tech/ for something that gets this right).

Ideally you work on a different enough bug that there's limited interaction, and ideally that's figured out before you fix it, but those criteria are indeed harder to satisfy in a bigger software.

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 much easier in comparison.

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 verification can be easier for higher-level languages.

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.

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 research on abstract interpretation, separation logic and so on.

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 a kind of UB they add options like `-fno-strict-aliasing` and pinky swear that option preserves the UB. I agree a useful checker should support real-world relevant C dialects.

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 agreed that the problem was unapproachable. Nowadays being a researcher is a job that requires steady progress, so you must focus on approachable problems. For P vs NP there are tons of results on classes of techniques that _cannot_ work—you'd have to learn those first to make a serious attempt.