fnrslvr

> Before Church, functions weren’t considered mathematical objects that could be passed as arguments to another function, for instance.

This strikes me as profoundly ahistorical. Mathematicians have considered function spaces as families of objects to be operated upon by higher-order functions (themselves considered objects to be operated on, and so on) long before the 1930s. I'm sure some version of this thinking has been part of the "folklore" of mathematics for centuries, but at the very least you have to recognize that the idea of higher-order functions is subsumed by Cantorian set theory in the 19th century.

Edit: if you mean to say that a formalism for higher-order functions was novel in its presence in a computational calculus, your remark makes a little more sense. But a few remarks on that:

* Already in 1933, Herbrand–Gödel μ-recursion had given a model of computation that was equivalent to the lambda calculus. (This could be the "recursion" that the post you're responding to was referencing.) I guess the μ operator could be regarded as a higher-order function, but functions don't really play a first-class role in the μ-calculus.

* It's probably more accurate to say that the lambda calculus was conceived as a logical formalism, of which Church published only a computational fragment when it became apparent that the original calculus was afflicted with the Kleene-Rosser paradox. Higher-order functions (and predicates) had already played a role in formal logic systems for decades prior to this.

You're reading a paper that analyzes the capabilities of a particular highly-constrained subclass of Turing machines. Actual research findings aren't necessarily going to be simple just because the model of computation being studied is simple. (Although a similar investigation into the capabilities of, e.g., a similarly constrained subset of Python, would probably tend to be a whole lot more lengthy and arduous.)

The parent's point is that the Turing machine model of computation admits a very concise definition -- roughly a page depending on brevity and formatting. An industrially viable programming language or hardware architecture typically requires a standard spanning hundreds of pages to define.

> My theory is that snippet and reply may lead to taking quotes out of context and replying with an uncharitable interpretation of the snippet.

My theory is that we're all so used to internet debates unfolding in snippet-and-reply-like formats that we associate snippet-and-reply with argumentative discussion by default.

A pedantic note, but what's happened here is that the companies involved have made a commitment to permit you to delete your data from the service. (Which they may or may not properly make good on, I'm not clear on whether they can be legally held to this commitment, e.g. in the US, once it's been made.)

A right to delete would mean something more like that the companies have no choice, e.g. that existing laws force them to delete your data from the service, whether they were willing to commit to offering that option or not.

> You could conceivably "race" searches between P and (not P) and hope that this would save you since now one of the two will return in finite time.

Adding to black_knight's point, it's worth noting that even in complete theories this often isn't very heartening: interleaving searches for P and for (not P) will often take an enormous amount of time.

Even cleverer strategies can be hopeless. For example, the theory of real closed fields is complete (and hence by your interleaving argument, decidable), but appears to be EXPSPACE-complete (at least from a brief skim of the literature), hence known to be truly intractable. If standard complexity-theoretic conjectures hold up (e.g. P != NP, NP != coNP), then non-gargantuan proofs in proof systems for a wide variety of interesting problems will turn out to be both intractable to locate and incomplete.

None of this is to say that automated theorem proving can't or won't rise to the level of human mathematical activity (I think it will fwiw), but we need to be far cleverer about it.

> while a classical mathematician will forever be tormented by the existence of theorems they cannot prove in their chosen formalism.

As a devotee to the law of excluded middle myself, I don't feel particularly tormented by this.

(I agree with your wider point that constructivism isn't the root cause of independent statements in mathematical foundation theories.)

If the headline question were something more like "can computers prove all theorems reliably?" this response would be more understandable. But a fairer interpretation would be "do automated theorem proving techniques stand a chance of making novel contributions to the mathematical literature?", to which I think it's pretty unfairly dismissive to rule out the possibility at this point. Considering it's still pretty early days for automated theorem proving, there's already some promising progress: an automated prover resolved the Robbins conjecture.

If you think Gödel's incompleteness theorems are hard evidence that computers can never consistently perform on the same level as humans at theorem proving, take it from someone who understands Gödel's results well: you're mistaken.

---

I think one sense in which the headline seems a little misleading, though, is that on a skim it looks like it's more about formalizing mathematical knowledge so that computers can verify theorems proven largely by people, than it is about computers themselves proving the theorems. (Which is also a fine topic, I'm not complaining.)

Whether a neural net could be trained to emulate a compiler seems like the more pertinent question.

I've had the displeasure of trying to explain classical learning hardness results to someone who kept repeating back to me "but RNNs are Turing complete!" If anything, the expressive power of the model you're trying to train pushes back against your efforts to train it to do something useful.

That would be a refutation of the claim that the calculation takes O(n) (or more correctly Omega(n)) time. If the center column turned out to be periodic, then yeah, you're basically on the right track: you would get an algorithm that runs in time polynomial in log(n).

I'm not sure how hard it would be to prove a lower bound on time for this problem, but if a polynomial space lower bound were proven (i.e. computing the nth square of the central column requires a Turing machine with access to Omega(n^a) space for some a > 0), then you'd have a sparse language in P that's not in L, which would be a huge advance for computational complexity theory. So definitely don't expect that anytime soon.

> Doing mathematics doesn't really depend on foundational logic in the same way that, e.g., a web app depends on transistor physics.

Web apps don't depend on transistor physics at all, though. An important consequence of Turing universality is that computer science is not a subfield of electrical engineering.

Also, mathematics underwent very dramatic transformations during the late 1800s and early 1900s alongside the early development of formal logic and set theory. To say that logicians were merely "formalizing the intuitions behind the math that people were already doing" strikes me as misguided at best. The mathematics that rose to prominence in that era was very different from what preceded it, often controversially so.

Okay, but that means that the era of vertical gameplay slices is effectively over, more-or-less exactly as described in the article. It further means that if a lack of gameplay demonstrations at E3 has left you feeling a bit unfulfilled (and maybe it doesn't, but it's a common takeaway among players following the event), then you only really have yourself to blame.

We might get a case study in this when Cyberpunk 2077 launches (possibly early next year!). CDPR, initially hesitant to reveal to the public the gameplay slice they produced for the media at last year's E3, eventually caved and released it with a prominent disclaimer watermark across the top of the screen:

"WORK IN PROGRESS - DOES NOT REPRESENT THE FINAL LOOK OF THE GAME"

As well as having similar messages reiterated by the narrator throughout.

Previously CD Projekt Red was roasted for perceived "downgrades" in The Witcher 3, notably in lighting which CDPR had to change to accommodate the day-night cycle in the game.

That said, hype for Cyberpunk 2077 is incredibly strong right now. We'll get to see whether players really do take disclaimer messaging into account when the final product launches, no doubt with "downgrades" evident in many facets of the game.

> As I understood it the large ones like No Man’s Sky or Anthem even doctored gameplay footage during their presentations

You're talking about vertical slices created years in advance of any realistic release date, for the sake of demonstrating to players a game that largely doesn't exist yet. Of course they're doctored. If they could show off natural gameplay, they'd have a near-releasable game and there'd be no need for the vertical slice.

> However when it was just "We might do this", then almost nobody blames them, a small minority might be angry or upset, but most don't care and many steps in to defend the devs in those cases.

When you start trying to make assertions about how "most players" responded, it becomes difficult to sort fact from fiction. "Most players" don't follow the games enthusiast press cycle -- whatever the perceived reaction to the press cycle for a game is, it's largely determined by the people who are the most engaged and the most vocal about the game in question, and it may be gauged differently depending on what slice of the reaction you were exposed to. That makes it pretty difficult to reach agreement as to what the temperament of the overall reaction was.

I also take a bit of issue with the expectation that designers should couch unconfirmed ideas with words like "might". It seems like an attempt to determine the validity of a wave of hysteria via a process of nitty-gritty word-lawyering that I don't think is very practical. Designers aren't always the best or most cautious of public speakers, so an idea that's in the "maybe" or "I hope" pile might not receive proper couching in suitable disclaimers when the designer speaks about it publicly. Further, players often don't remember the full context of words that are spoken about a game, and even are likely to want to read the most enticing thing possible out of the words written or spoken about a game they're intentionally following. Insisting that words that are publically spoken about a game in production are lawyerable like this just encourages studios to clamp down and stop speaking to the public about their craft, and leaves us with sterile messaging that's been carefully crafted by PR experts.

With that said, I'd counter that there's a pretty lengthy history of players misinterpreting the exploratory words of designers about possibilities for their in-production games as promises about what the final product would contain, and then later raking them over the coals for breaking those promises. On the spot I think that's going to be a tricky view to corroborate without going through a messy and time-consuming process of picking apart a bunch of case studies, though.

Set theory and logic are too interdependent to venture far in one whilst steering clear of the other. For instance, you'll only really skim the surface of model theory without a basic understanding of infinite cardinals.

Set theory as a toolkit is mostly geared towards questions of consistency/existence, size or "order" of objects, and raw mathematical explanatory power of theories or claims. It traditionally arose to explore ideas of infinity precisely, then grew to meet the needs of a mathematical community grappling with antinomies (e.g. Russell's paradox) and heated foundational divides (classicism vs intuitionism, etc). It still meets those needs well -- topics like large cardinals which chart the territory dangerously beyond the boundaries of (assumed) mathematical consistency are plied with set theory, and questions of consistency that arise in other fields tend to end up ported into set-theoretic terms.

I'm not a type theorist, but I imagine the split between set theory and type theory is analogous to the way in which different models of computation appeal to researchers on different sides of the "Theory A/Theory B" split in computer science. Researchers in the "A" group who study the outer limits of what problems are/aren't tractable, how different kinds of computational resource compare in power, etc, tend to use Turing machines and RAM models and circuits, which allow computational resources to be easily measured, bounded, simulated, reduced into things, etc. Researchers in the "B" group who explore programming languages, type systems, program analysis, etc, tend to prefer models like lambda calculus which allow programs to be easily composed and annotated with types and whatnot. I don't think this is just about cultural differences -- if you try to prove time-space trade-offs with the lambda calculus or invent a new type parameterization system with Turing machines then you're going to have a bad time.

Are you familiar with the story? The COO of Riot has been accused of ball-tapping and humping employees. I don't know about you, but if someone "ball-tapped" me in a workplace, I'd be reporting the incident to HR as sexual harassment.

lol, both pivotal sources that I'll swiftly consult when something in my browser goes haywire.

Seriously though, when I checked the Mozilla and Firefox twitters (and I don't use twitter, so even going that far was a stretch for me) just before I wrote the parent post, they hadn't gotten around to tweeting a notice about this there, either. The Mozilla Add-ons twitter account is not the highest-level place that should be talking about this situation.

Yeah, I guess I could see people coming in with that take. Personally I'll gladly accept a tether to the mothership if they offer the choice.

That said, I regularly get thinkpieces from Mozilla about the open internet, privacy, requests for donation (which I often oblige), etc., in my inbox. They also drop notifications under the address bar and in a "Message from Firefox" bar at the bottom of the new tab page, which I got the impression they had some live control over.

But maybe not, and/or maybe there's a long runway on preparing correspondence by any of these channels for some reason. If anything, I hope that when they do get around to getting some wide-reaching messaging out there, they indicate that they plan on doing the work to shorten the runway on emergency messaging in future.

Mozilla doesn't seem to have communicated the issue well. I could imagine a lot of unsavvy users have tried some wild things in an attempt to fix the problem, and maybe made a mess in the process. Doesn't Mozilla have a mechanism for blasting out a message to all Firefox browsers? Also I have a Firefox account, why haven't I been inboxed about this?

Otherwise I'm not bothered. I won't be switching as long as this gets resolved within the next few days.

I'm not sure I see where objects enter into this. I mean, you seem to be asking for something like this,

  public unit Util {
      public void foo() {
          // do things
      }
  }

which would compile down into a bytecode-containing artifact which we could call a unit file, which the JVM would load at runtime using some sort of unit loader. Callers could import the Util unit and then invoke foo with the statement

  Util.foo();

But then, I don't see the diffence between the above and the following,

  public class Util {
      public static void foo() {
          // do things
      }
      // If we're really pedantic, we can ban construction of Util instances
      private Util() {}
  }

which compiles down into a bytecode-containing artifact called a class file, which the JVM loads at runtime using a class loader. Callers can import the Util class and then invoke foo with the statement

  Util.foo();

What's this downside you speak of? Is there something a different kind of translation unit would do that a class currently doesn't?

> I think this is a fundamental error since functions and data structures belong in totally different worlds.

This is my biggest issue with the article. Blurring the boundary between program and data is one of the core principles at the heart of computer science, and was crucial to the works of Turing, Church, et al, that birthed computer science as a field.

> You could also make a class of global functions and use that

I'm not sure I understand your issue with doing this. You need to put your global (i.e. public static) functions in classes not because Java is forcing OO practices into everything, but because classes effectively serve as Java's translation units. I think they serve this purpose pretty well in practice.

> Imperative programming languages (like C and JavaScript) don't generally impose any discipline on the users.

I think this view disrespects history a little. C was one of the earliest languages to be conceived upon a foundation of structured programming principles, i.e. block structure, sequence/selection/repetition, subroutining. (Okay the language still has goto, hopefully we can agree to not make a big deal out of that.) The kind of discipline proposed by structured programming was far from universally well-received at the time, and I think it's fair to say that it lead to huge improvements in the quality of codebases everywhere, and is one of the great successes of programming language thinking of the '70s.

C is also statically typed. It's obviously easy to blow all sorts of holes in C's type system, but if you'd go so far as to say that C's types impose no discipline at all, I'd ask you to try teaching C to a room full of compsci students who have been raised on something like Python.

I'll add, that I strongly advise against beelining for Gödel's Incompleteness theorems.

Learn the formal language aspects, like grammar and parsing and structural induction. Learn semantics. Learn a few deductive calculi (say, natural deduction and Hilbert style) and how they interrelate, and actually use them to prove some (very simple) results, ideally from some important axiom systems like Peano arithmetic and ZF set theory. Learn model theory, Gödel's completeness theorem, the compactness theorem, and their more immediate implications.

You should also learn how logic interrelates with

* Computation, both in the sense of enumerability of deductive proof systems, and in the sense in which expressability in certain logical theories is Turing-complete; and

* Set theory, both to grasp the sense in which a first-order set theory like ZF seems to suffice to supply an ontology for the rest of mathematics, and to understand the role of cardinality in e.g. model theory.

There isn't really a correct order in which to approach these fields. You'll find that for a proper understanding of any of these topics, you'll have to move back and forth between them frequently.

I would put off Gödel's incompleteness theorems until you've done most of this. In particular, learn the completeness theorem, up to a point of confidently being able to apply the compactness theorem, first. Many of the least-informed abuses of the incompleteness theorems come from people who can't distinguish different notions of entailment, and are unfamiliar with the successes of deductive calculi and the categoricity shortcomings of first-order logic.

> Mathematical Logic

A Mathematical Introduction to Logic, by Herbert Enderton.

I haven't seen the code, but maybe c&p-ing the C entrant into the C++ box to get performance parity would make the C++ entrant run afoul of typical C++ coding conventions.

(You can then have a debate about whether you want to see idiomatic C++ in benchmarks or purely the most performant C++ possible. Personally if I'm shopping for a language for a project then I'm far more likely to be interested in the former.)

> Steam is popular and has a loud following because it does not make unethical choices that annoy users.

Not true. Valve fought (and lost) a drawn-out legal battle against the Australian Competition and Consumer Commission over the rights of consumers using Steam, including right to refunds: https://www.accc.gov.au/media-release/full-federal-court-con...

The outcome of this case paved the way for Steam's current refund policy.

Adding to atq2119's answer, integer programming is merely NP-complete. You really need full Turing computability to get the incompleteness results. The set of provable consequences of Peano arithmetic is RE-complete, and we know that NP != RE, so you definitely can't give an integer program that verifies that a formula is provable from PA, which is a necessary ingredient.

To be fair, recent grads also have an enormous amount of trouble breaking into the industry. The prisoner's dilemma of training up the graduate at a negative return for 2 years before watching them get poached is an issue that's been thoroughly canvassed around here. I think it's beneficial to the health of the industry that tech giants are at least somewhat willing to calibrate their hiring processes towards that class of applicant and take on that risk, and I hope they don't move away from that just to even further pad the career prospects of people with 5-10 years' experience.

Because I want full encapsulation without giving up by-value semantics. I want my clients to be able to take objects of some opaque record type that I've defined, and put them entirely on the stack, or in some contiguous block of memory entirely of their making, without ever getting to know the constituent fields of the record. I want it all, I want to have my cake and eat it too.

When the parent (er, great grandparent?) says their parent is wrong to deny that headers only reveal the interface, I think it's a little disingenuous to base that on an unrevealed assumption that PImpl is in play. PImpl is basically the the idiom that begot Java. One reason I might opt for C++ over Java, is a desire for finer control over the location of memory -- but it's important for me to know that to actually get that, I'll probably have to sacrifice information hiding. It's a trade-off. Yes, on some level it's better to have the option to make that trade-off, but the product here is "encapsulation or value semantics", not "encapsulation and value semantics".

Mind, I'm not a C++ developer. Maybe these days link-time heroic optimization makes the "right" decisions and collapses these kinds of indirections in all the sorts of situations you'd want it to. I write a lot more Java, and my understanding is that HotSpot gets up to a lot of heroics pertaining to this stuff these days -- I've noticed HotSpot will churn through a workload involving processing a collection of records far more quickly if you can arrange for it to stream through an array, even if you'd expect the records to be scattered randomly throughout memory.