Is the "optimal Julia workflow" written down anywhere?
5,792 karma · joined January 31, 2020
At the end, the author notes (as you do) that if you consider a finite difference equation with small time steps, there are no pathological solutions. He also mentions that Newton takes this difference equation approach when solving problems in his Principia.
See also "The Norton Dome and the Nineteenth Century Foundations of Determinism" by van Strien:
>> Abstract. The recent discovery of an indeterministic system in classical mechanics, the Norton dome, has shown that answering the question whether classical mechanics is deterministic can be a complicated matter. In this paper I show that indeterministic systems similar to the Norton dome were already known in the nineteenth century: I discuss four nineteenth century authors who wrote about such systems, namely Poisson, Duhamel, Boussinesq and Bertrand. However, I argue that their discussion of such systems was very different from the contemporary discussion about the Norton dome, because physicists in the nineteenth century conceived of determinism in essentially different ways: whereas in the contemporary literature on determinism in classical physics, determinism is usually taken to be a property of the equations of physics, in the nineteenth century determinism was primarily taken to be a presupposition of theories in physics, and as such it was not necessarily affected by the possible existence of systems such as the Norton dome.
Best practice (as I understand it) is to fix the model ahead of time, before seeing the data, if possible (as in a randomized controlled trial of a new medicine, etc.).
1. Typically we use p-values to construct confidence intervals, answering the concern about quantifying the effect size. (That is, the confidence interval is the collection of all values not rejected by the hypothesis test.)
2. P-values control type I error. Well-powered designs control type I and type II error. Good control of these errors is a kind of minimal requirement for a statistical procedure. Your example shows that we should perhaps consider more than just these aspects, but we should certainly be suspicious of any procedure that doesn't have good type I and II error control.
3. This is a problem with any kind of statistical modeling, and is not specific to p-values. All statistical techniques make assumptions that generally render them invalid when violated.
I dislike the paper because it is sensationalist and highly misleading. For example, as far as I can tell, Karplus and Kroll didn't "confess" to anything (no direct quote is provided in the paper); we just have a secondhand assertion by Feynman. Nothing they did is "fraud," as the author claims - this is false and defamatory. Further, the issue got wrapped up by Petermann in 1957; the author is just annoyed that he didn't publish full details of the calculations. The suggestion that there is somehow lingering uncertainty is just wrong.
I no particular wishes for the author, other than that he cease writing bad papers.
The summary is that the author doesn't know what he's talking about.
As someone who has learned and taught a lot of math, I agree with that claim.
Further, the result in a recent replication [1] was a correlation of .28 between the time to ring the bell (to get the marshmallow) and academic achievement. That's not exactly the trivial "4% less likely" effect in your caricature.
(You may also wish to double check your spelling of "marshmallow.")
[1]: https://www.jasoncollins.blog/posts/the-marshmallow-test-hel...
My challenge to you: find a single book written in the last, say 50 years, where the answer to this question is not ZFC (or ZF with some equivocation about whether we should accept choice).
Re: "Equivalence is equivalent to equality," first of all, most mathematicians would take this to be false. Like, if "x" stands for cartesian product, they would say (A x B) x C and A x (B x C) are different objects. (This is a point commonly made in undergraduate algebra classes, and the reason they would say this is of course they they implicitly think of everything as sets, since set theory is the standard foundation!) They are isomorphic objects, but not equal ones. Second, to the extent that mathematicians suppress isomorphisms like this in their writing, this is not a new observation. We've known that mathematicians do this for decades, and in principle we could always unravel such isomorphisms when writing things down carefully if we needed to. This is not some special insight of HoTT. Compare to the forcing example I gave - this is a genuinely new insight about the Calkin algebra facilitated by "classical" methods of mathematical logic.
Re: DNNs, the question of what is a semantics for DNN does not count as an example, no. What would count: statements about things like consistency, independence, shapes, numbers, etc. It's cool that you can use HoTT for engineering things but it's not an application to discovering new pure mathematics or the consistency/proof strength/independence/etc. of that mathematics. The latter is the usual definition of "metamathematics."
Here's an example of a (true) metamathematical statement: HoTT is consistent if ZFC plus two inaccessible cardinals is consistent. (Interestingly, this is the best argument I'm aware of for the claim that HoTT is consistent, and its power derives largely from the fact that ZFC is the Gold Standard for foundations.)
Facilitating metamathematical inquiry of this kind is perhaps the primary reason mathematicians are still interested in set theory and classical logic. (I include here large cardinals, model theory, etc. For further discussion, see the books I mentioned above.)
Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" You proceeded to give examples that did not fit this description. If you agree that HoTT is not good for metamathematical inquiry, then great, we agree on something!
Also, DNNs are (definitionally) not a topic in pure mathematics.
1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice.
2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean).
My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals.
3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others.
Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic.
4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.
Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
> Are there any which don’t exclusively apply to the mechanics of set theory itself?
Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others.
> That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).
> But the whole point is how to keep track of what questions one is evidently allowed to ask - what questions are demonstrably not as ill-posed as "is the number 7 equal to the trivial group".
I don't understand what you mean by "questions one is evidently allowed to ask." You can ask any questions you want. In particular, as long as we agree that whatever question you want to ask can be translated into a question about sets, we can resolve that question by answering the analogous question in the framework of ZFC. All I object to is the claim that some set is, ontologically speaking, the same as the number 7, and hence that set theory proves "junk theorems."
Here's a silly analogy. Suppose we work at NASA and we want to fly a rocket to the moon. We agree that the answer the question of how much fuel we need, we can write a computer simulation with a representation of the rocket, the earth, the moon, and so on. We run the simulation and answer our question in that simulation, and if the simulation is a good representation of reality that also answers our question in reality, and then we go to the moon and everyone is happy. However, nowhere in this process do we believe that the rocket in the simulation is the same thing as the rocket IRL.
> You're very dogmatic about what people should accept from a foundation. You seem happy to accept an approach that has very little to say about practice, which is certainly an opinion, but not universally held.
> There is a point of view that foundations should reflect and inform practice - or maybe even challenge practice - and are not just there to make you feel more comfortable philosophically.
I don't understand this comment. Studying set theory has said a lot about mathematical practice - for instance, about what we can and can't hope to prove in certain systems, or about what axioms are needed for what statements. That's important stuff!
More generally, there's the question of what you hope to accomplish by supplying a foundation for mathematics. Any value claim about some foundational system is contingent on what goal you have. As I said above, if that goal is actually writing down computer-checkable formalized versions of complex proofs, then ZFC is perhaps not the foundation you want to use.
But, historically speaking, that was not what people had in mind. There was a desire to reduce mathematical reasoning to a few philosophically basic concepts so that we could be confident in its coherence and consistency. And a desire for providing a framework for studying mathematical reasoning itself. I think it's really important to understand this historical context, otherwise you end up with misleading claims like "ZFC is a bad foundational system because it doesn't help me formalize my research papers."
Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics (or even exist on equal footing, creating a plurality of foundational systems). If you take the goal of a foundational system to be practically formalizing proofs, we have no evidence HoTT is particularly suited for this, and (as far as I know) no serious movement by the HoTT community to actually realize this vision (relative to what the Lean community is doing). I'm not claiming the first mover in some space should always dominate, just that if the HoTT people want to arguing for their foundational system on the grounds that it assists in formalizing math, maybe they should actually demonstrate their superiority by formalizing some math. For a longer comment on this, see: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....
So if we disregard formalization, the arguments in favor of HoTT that remain are philosophical ones. But, as I've explained elsewhere in this thread, I find them all misguided. They all basically seem like arguments about aesthetics but don't actually tell me why HoTT is better than ZFC for the philosophical goals mentioned above.
ZFC hasn't been "replaced" by anything. The standard line in all published textbooks that I'm aware of is that ZFC is the accepted (by the professional mathematical community) foundation for doing mathematics (assuming this question is even raised). Even the type theorists admit this!
> That’s why we replaced Turing machines with type theories, lambda calculus, automata, etc. Our modern research uses these formalisms because they’re outright better.
The Turing machine is a fundamental concept in theoretical CS that isn't going anywhere. Consider that the standard textbook on the theory of computation (Sipser's) has three parts, and the second is entirely devoted to studying computability using the Turing machine concept. Or that the strength of pushdown automata is usually explained in relation to Turing machines.
> OK, so what are the concrete fruits of this?
The first two things you listed are not metamathematical statements. I'm not sure what you mean by the third. (Sure, many things can be recognized as special cases of category-specific concepts. But that's a claim about category theory, not HoTT.)
> This is also a weird demand while leading off with how people don’t actually work in ZFC.
People do not write their papers in first order logic starting from the ZFC axioms, that's true. But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
> Nevertheless, topos theory is what explains the algebra-geometry duality: you have two languages (type theories) that map to isomorphic categories. You can then extend that idea to things like the Curry-Howard square.
OK, so what's the actual concrete statement an ordinary mathematician should be interested in?