In higher math (typically 2nd year and onwards at US universities) there is fairly little explicit calculation, and math is more about studying the (formal) relationships between mathematical objects. For example, we can abstractly define topological spaces and abstractly define algebraic “groups,” and algebraic topology studies the relationships between topological spaces and algebraic groups. This is somewhat like having a “data type” defined by some library, examining ways it can be transformed into data types defined by some other library, and studying what invariants hold under those transformations.
In some sense, an undergraduate math education is akin to learning the “standard library” (in the software engineering sense) of higher mathematics. Most courses start with basic abstractions of some mathematical object and repeatedly construct more and more abstractions on top of those. The structure of those abstractions is similar to how you might build a library. A professional mathematician is expected to be fluent in the mathematical standard library, just like how you might expect an experienced software engineer to be fluent in Python’s standard library.
If this analogy is true, people who can learn Python relatively quickly might be able to also learn higher mathematics relatively quickly under the right pedagogical environment.
One personal project I'd love to find the time for is to try to write out a sequence of math notes that essentially builds up a Lean repository, intentionally "refactoring" as it goes along. So you do some explicit coordinate vector or system-of-equation calculations with both real and complex numbers, eventually define interfaces for fields and vectors, do your linear algebra proofs, realize that linear endomorphisms are almost-but-not-quite a field, so define rings and go back and refactor your field proofs to use them, realize vector spaces are "K[T] not-quite vector spaces", define modules, refactor your vector space code, etc.
This was kind of how math classes worked, but without that explicit phrasing. It would certainly make the analogy between the two activities more obvious. I also wonder whether people would have less trouble with quantifiers if they were phrased in programming terms: a proof of "forall x, p(x)" is a function x=>p(x), and a proof of "there exists x such that p(x)" is a pair (x, p(x)). e.g.
proof of UC => C = (epsilon, h, x_0) => let delta, h2 = UC(epsilon,h) in (delta, h2(_,x_0,_))
So when you're trying to figure out how to do the proof, it's clear what kind of type you need to return and your IDE could help you with autocomplete based on type inference.
You know more than fresh graduates, but fresh graduates don’t absorb 100% of the material being taught — more like 50% at best, and many promptly forget that knowledge after taking the final. As someone who went back to school after about five years in SWE industry, I did (and still am) learning things in CS classes.
Granted I did know a lot of the material already, and I do go to Berkeley which has a comprehensive CS program, so YMMV. My main point is to not compare your knowledge to fresh grads knowledge to determine what they are taught.
Alphabetical is the norm in algorithms theory. It is not the norm in other subfields that I can think of, even theoretical fields like programming language theory.
> Wouldn't extracting too much energy from the earth's core cool it down, at least a little bit?
The earth generates ~50 terawatts of energy through radiation/other processes, while global energy consumption over the last year was 0.003 terawatts. I think we're fine.
Where are you getting 0.003 terawatts? Another user elsewhere in the thread[0] claimed "Global total energy (not just electricity) consumption is currently 180,000TWh/year, or about 20TW."
Google is showing me other figures like 25,000 terawatt hours of electricity consumption annually.
One might also be careful to count energy properly. The fossil fuel industry has been counting "total energy" including losses to make fossil look bigger and harder to replace. But a gas car throws away like 70% of the energy, so going electric, you don't need the same energy to run the car. Not even close.
Nit: the correspondence between phi-SSA and basic block arguments is not one to one. With block arguments, you can jump to the same block with different arguments depending on a condition. You can’t do that in SSA without adding new blocks.
Is there a specific issue with more context? I looked at the repo already but it’s not obvious which operations are slowest / most important to optimize.
My guess is that without operating system support or equivalent, there is not an easy way to avoid extracting the zip file. (You could patch syscalls in the Python interpreter to read from the zip file for certain paths, but that might be hacky.)
I did find https://github.com/google/mount-zip which might be useful, but you would likely have to still mount the zip manually. However, you don’t have to worry as much about cleaning up after yourself.
reply