gnulinux

Just in case people consider this seriously, I just want to add my two cents: Ulysses although is prose, it's so much more of a poetry than prose compared many other novels. I personally don't think listening to someone's reading of Ulysses will be remotely similar to reading it on page. Some of the chapters are really almost entirely about discovering how to read this chapter. I don't necessarily think it's bad, just the same way you can listen to poetry by going to a poetry reading session, you can listen to Ulysses. Just note that it's going to be an entirely different experience than reading it, and it will likely forever bias your interpretation of the book. Just my humble two cents, I don't claim to know anything.

This is extremely true. Reading Dostoyevsky as an adult was like finding a long lost treasure in ancient scrolls. I never understood what's the point in High School. Some of the classics are really classics because they're so much about humanity at large, and unless you're a literary prodigy like Rimbaud or whatever a lot of human drama won't make sense to you in high school--maybe even then. Schools really blew it out of proportion by assigning books like Crime & Punishment, Ulysses etc to 16 year old kids who are essentially overgrown toddlers. I think kids should still attempt to read these books in High School (learning comes from challenge) but creating the entire curriculum based on these adult books does them a disservice by not answering the "why do we give a shit?" question.

Really, same thing goes for most other disciplines. So many kids learn 4 years of algebra without having the slightest clue that this all is building to something called "Calculus" that they don't understand what it is.

I implemented the same in some of my programming languages. If you look into very generic mixfix operators in some languages like Agda, you'll realize that operator precedence is a mess and it feels so much better to get rid of it. Of course, it makes the language unusable as a mainstream language, but it makes so much more logical sense.

Disclaimer: Never used Ibis before but I daily use polars and DuckDB.

It seems like Ibis uses DuckDB on its backend (by default) and has Polars support as well. Given this, maybe see if Ibis works better for you than polars. If you very specifically need polars, using that will for sure be better. DuckDB is faster than polars and it has great polars support, so depending on how Ibis is implemented it might be "better" than polars as data frame lib.

It's not that it's a proxy for memory use, but FD is its own resource, I've seen many software with FD leak (i.e. they open a file and forget about it, if they need the file again, they open another FD) so this limit can be a method to tell that it's leaking. Whether that's a good idea/necessary depends on the application.

Why not? Why do you think it's irrelevant? The reason why I included that is very simple: it models the situation I want to express exceptionally well. In "mathematics" we learn in school none of the discussion relevant to the "Halting Problem" really is relevant, which is very confusing to students who even paid attention in school. To make the situation even relevant, we need to start assuming (or realizing, accepting, whichever one you want) that there are relations in mathematics that are undecidable. If you have a model of computation, which will internally be constructive, in order to freely apply our knowledge of mathematics onto this model, we need to go back to grade school and replace every instance of "is true" with "is constructible in your model of computation/programming language" (or more traditionally "is provable"). Which means you need an entirely different reasoning framework. So, to "go back" to classical math from having understood the existence of undecidability as "home", we need to unassume this, which will be identical to assuming all relations are "decidable" within your computational model. It's not like they actually are (at least not to the extent you can compute within). Homotopy theory is the exact thing that's developed to explain situations such as this one. Why not just use it? I apologize if anything I say is wrong or misleading, I'd be happy if you can clarify.

The reason decidability makes no or very little sense to tons of CS or Math majors is because the logical basis of decidability is almost never explained in school. Even if you're in a logic/computability class you likely won't get a very concrete explanation, unless you're in a Philosophy of Math class.

The problem that's usually not told to kids is that decidability has different sort of implications to classical mathematics and constructive mathematics. Since most undergrad programs only teach mainstream math (i.e. classical) and don't even mention constructive logic, decidability becomes a black magic situation for some confused students.

Here's the crucial part: decidability really only has material impact on our reasoning if we're in some kind of constructive setting. Undecidability does not and cannot have any impact on the results of classical mathematics, period, but it does have effect on the proofs of those classical theorems. It can also have impact on classical mathematics if we're reasoning classically but describing results in constructive settings (e.g. this is what happens when we do computability theory in classical mathematics).

In short, classically we're always allowed to work around undecidability by using an "oracle". But it can be important to state that we can only do it this way (similar to how we can state the need to use the axiom of choice).

One way to re-phrase Aristotle's law of excluded middle (forall P, P or not P) is to say: "every relation is decidable" which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd...

This doesn't mean in classical mathematics every relation "literally" is decidable. Classical mathematics can still study constructive settings by creating a computational model (e.g. Turing Machine model). But it does mean that in classical mathematics every relation effectively is indistinguishable from decidable relations since given a statement like "Program P will halt" you are always allowed to say "either (program P will halt) or (program P won't halt)" regardless of our impossibility to prove one of the cases in general.

Also note that we call this kind of constructive reasoning "neutral constructive mathematics" which is when we operate in a constructive reasoning setting (like Agda's type theory above) but allow ourselves to say things like "AxiomOfChoice implies ExcludedMiddle" etc, read: https://ncatlab.org/nlab/show/neutral+constructive+mathemati...

I just Ctrl+P print the reader mode output to PDF. Takes 1 second. I've been doing it for years and it works perfectly. I have articles I saved from a decade ago in Dropbox. I'm honestly surprised people use a whole app for such a trivial feature, but yeah it's fair to have special needs. For me, Firefox reader mode is all I need, and you can just save it as PDF.

I personally prefer Agda to Lean or Coq [1] to prove my theorems but this frontier is imho among the most exciting research in theoretical CS in many many decades. I really wish more programmers and mathematicians knew about automated theorem proving and automated reasoning. It's nothing short of revolutionary and I think next generation of pure mathematicians will use these as a crucial tool in their research.

[1] It's a personal preference but Agda is simply a much better language with almost limitless metaprogramming which allows me to write proofs close to as they'd appear in prose math papers. It has a smaller ecosystem though. I've never seen a proof in any other language I personally didn't think would be much more readable/simpler in Agda.

Principia was written during the naive Logicist era of philosophy of mathematics that couldn't foresee serious foundational decidability issues in logic like Godel's incompleteness theorems, or the Halting Problem. Formalism/Platonism and Constructivism are two streams that came out of Logicism as a way to fix logical issues, and they're (very roughly speaking) the philosophical basis of classical mathematics and constructive mathematics today.

The way formalists (mainstream mathematical community) dealt with the foundational issues was to study them very closely and precisely so that they can ignore it as much as possible. The philosophical justification is that even though a statement P is undecidable, ultimately speaking, within the universe of mathematical truth, it's either true or false and nothing else, even though we may not be able to construct a proof of either.

Constructivists on the other hand took the opposite approach, they equated mathematical truth with provability, therefore undecidable statements P are such that they're neither true nor false, constructively. This means Aristotle's law of excluded middle (for any statement P, P or (not P)) no longer holds and therefore constructivists had to rebuild mathematics from a different logical basis.

The issue with Principia is it doesn't know how to deal with issues like this, so the way it lays out mathematics no longer makes total sense, and its goals (mathematical program) are found to be impossible.

Note: this is an extreme oversimplification. I recommend Stanford Encyclopedia of Philosophy for a more detailed overview. E.g. https://plato.stanford.edu/entries/hilbert-program/

I'm sorry I know this is horrific but I still love it. This looks like a better version of Boost Lambda2. I would potentially maybe replace `$` with `_` before using this (which should be easy as a layer) like Boost::Lambda2 but otherwise I'm excited to use it. Not that I would use anything like this in production, but it looks too fun not to play around with.

It's not at odds at all but it'll be "Monadic" in the sense that the output of system A will be part of the input to system A+1 which is complicated to organize in a systems setting, especially if you don't have access to a language that can verify. But it's absolutely achievable if you do have such a tool, e.g. you can do this in nix.

> Teotihuacan rather famously was not a literate society

Isn't this going a bit too far? Sure they didn't have a modern writing system like Mayans, or even proto-writing systems like Inca's quipu but we do have hard evidence of Teotihuacan society communicating language with painted symbols (e.g. findings in La Ventilla). It's unclear to me how we can say they didn't leave writing to future generations (especially assuming probably there were a lot more stuff that was lost to time than we can see)

Also, this comment seems to slightly misunderstand what the GP said imho. Yes writing is a new invention, but e.g. paintings in Lascaux are about 17k years old. Which means even before Catalhoyuk level civilizations, humans were leaving symbols for later generations to look and decipher. This is the same "archival" process GP is talking about. Humans leave a message to future generations. It seems like our biology must prime us to do it, because we see it universally. Whether the messages we leave are writing, painting, music or whatever... humans still produce things for people that'll come after them. But animals are incapable of doing so, even if a Bonobo is roughly as intelligent as a human, it's not like it can transmit any kind of information to future generations, so every generation of Bonobos need to learn either from scratch or from their community. So, perhaps ironically, part of being human-smart is having human-precise hands that can paint/write. Without this ability, we end up like bonobos, elephants, dolphins etc perhaps smart but for all they know their parents were the Adam and Eve.

> if I told you 10yrs ago that we'd have AI that can do math/code better than 99% of humans

This not even remotely close to true. Like not even a little bit. I use Cursor and Gemini for work daily and I'd be hard pressed to think AI is a "better" programmer than any professional software engineer. Sure it makes writing code faster and more efficient, because you just click tab and three lines are written for you. It absolutely isn't better than me at coding though.

The claim about math is even more unbelievable than the claim about coding. We still don't have a single theorem proved and published by a LLM without human aid. LLMs barely follow a discussion in basic topology. It's incredibly ridiculous to state they're better than 99% of people. More like 0% of mathematicians and maybe 50% of college freshman.

I don't see any issues in Android Firefox, works pretty much the same as my OSX Chrome or Firefox. What is the problem you're having I wonder?

My boss regularly criticizes me for thinking too much. Sometimes I stop and think if this is the best way to implement something, and then suddenly receive a lecture about velocity, moving fast, being efficient, being ok with pushing bugs to prod, and all that shebang.

Our society has a pathological obsession with productivity.

You can absolutely do this with hypothesis stateful testing. https://hypothesis.readthedocs.io/en/latest/stateful.html

DuckDB is mind blowingly awesome. It is like SQLite, lightweight, embeddable, serverless, in-memory database, but it's optimized to be columnar (analytics optimized). It can work with files that are in filesystem, S3 etc without copying (it just looks at the necessary regions in the file) by just doing `select * from 's3://....something.parquet'`. It support automatic compression and automatic indexing. It can read json lines, parquet, CSV, its own db format, sqlite db, excel, Google Sheets... It has a very convenient SQL dialect with many QoL improvements and extensions (and is PostgreSQL compatible). Best of all: it's incredibly fast. Sometimes it's so fast that I find myself puzzled "how can it possibly analyze 10M rows in 0.1 seconds?" and I find it difficult to replicate the performance in pure Rust. It is an extremely useful tool. In the last year, it has become one of my use-everyday tools because the scope of problems you can just throw DuckDB at is gigantic. If you have a whole bunch of structured data that you want to learn something about, chances are DuckDB is the ideal tool.

PS: Not associated with DuckDB team at all, I just love DuckDB so much that I shill for them when I see them in HN.

I'm personally very sympathetic and interested in avant-garde, experimental software development methods like this. I understand that most devs reading this is mortified and doubt about my sanity, but I do unironically use extremely, stupidly limiting techniques like this. For example, in my current project (working on an automated theorem prover) I have this rule that development happens in epochs. I write code in file theorem_prover_v1.rs, I run some unittests, run some tests, take notes. Copy the file to theorem_prover_v2.rs and attempt to rewrite the whole thing based on the previous form. Every line is critically examined. As many lines are attempted to be modified as possible. Do we need this type? Is this mathematically sound? Can I really justify that this abstraction is necessary? [1] It's an extremely inefficient and slow process, but a lot of software engineers don't appreciate that development efficiency--although usually among the most important factors of the success of the project--it's not necessarily the only important factor for all projects, and it is worth experimenting with methods that are intentionally inefficient but has promise to improve something else. You don't like it, you can always go back to Agile or whatever else you do at your day job.

Art progresses with extreme restrictions. The same way Schoenberg put seemingly absurd restrictions in his music ((very roughly) don't repeat the same note before playing every other note etc...) to create something radically novel, we as software developers can do so to advance our art as well.

[1] This method is the anti-thesis of the common "never rewrite a working program" software development methodology. Here, the experiment is to see what happens if we always rewrite, and never add or modify, i.e. refactors are never allowed, instead if things need changing we need to re-design the whole thing top-bottom with the new understanding.

They are related and the reason is the last point of the OP article: Abstraction. Things can be "physically" deterministic, but can be abstracted as non-deterministic. This seems strange at first but it actually makes a lot of sense, as long as you're not modelling physics itself, it's irrelevant that there is a theory in which your non-model is deterministic. Machine learning algorithms like ChatGPT can be good examples, given the exact same input+random seed, of course, they'll return the same exact output, but the situation is so computationally complex that modeling that system as deterministic is less useful than modelling it as if it's non-deterministic. This is the same way your computer RAM is not "infinite"--it's like trillions of bits-- but in CS we model it as if it's infinite because the practical difference is not the focus of the discussion. If the discussion really was "can we fit a pigeon in every bit of my computer" or "can we manufacture every bit of this RAM in finite amount of time" then yes, it would be relevant to argue that RAM isn't actually infinite. But given that we're interested in models of computation that get exponentially larger and larger as memory grows, even 10 bits can be an intractibly large space (cf. Busy Beaver numbers) so you might as well solve the problem as if it's infinite.

You can also use a different but similar tool e.g. use sqlite to keep user information, use duckdb to keep user data. I find this combo very effective since sqlite is best as fast btree based indexed operations and duckdb is best at multiple row based aggregate computations (get me user X vs get me all users with property Y).

This is a lovely comment and I agree with your list. At least, it's been my experience.

Did you read the executive order? It clearly states it also covers parents that are here legally through visas like H, F etc... It is not just about illegal immigration. E.g. if you work in the US on H and have a kid with a student on F visa, the kid will not be a US citizen going forward (starting in 30 days).

I'd be curious to hear the argument that people legally working or studying here aren't "subject to jurisdiction" of. People on H1B for a while file the exact same taxes citizens file (because they're US persons for tax purposes). Not sure how are they legally not subject to jurisdiction of?

I didn't say Western music is anti-human. Treating it as the only possible form of music is.

The difference is in the model. The same way you can model mechanics with Newtonian mechanics, or statistical mechanics, or quantum mechanics and each of them can be useful in different scenarios, and irrelevant in others.

If you're making Western classical music in classicist, romanticist or modernist style, the model of music you have will carry a lot of information about harmony and the application of harmonic techniques throughout the piece. Given a core musical idea you can then apply peripheral techniques (such as orchestration) to build a full piece. E.g. when people study counterpoint, the model of music originates from vertical harmony of notes and when they can be used with respect to each other. The assumption is that orchestration is something that'll be separately developed "skinning" the composition. E.g. a common technique in this tradition is composing a piece for piano four hands and then orchestrating it (e.g. Holst's "The Planets" symphony was composed this way).

However, this stops being a useful model once you step into other musical traditions. In some cultures harmony would be like how Western music treats orchestration, peripheral to composition (like how extreme speed is irrelevant to Newtonian mechanics because it was never designed for near lightspeed motion). So you'd first design timbres, and have an idea about how timbres interact, timbres change, transform to each. You may have a theory of counterpoint of timbres. Once you have this, you can apply any standard "harmony skin" on the composition and you have a piece. This is not even restricted to non-Western music. If you look at the postmodernism in Western music you'll find instances of it. Easy example: a lot of people say that Philip Glass "makes the same music" again and again, what is being missed is the point he's trying to convey is that even if you pick the exact same 4 chords you can still create variation in music via other means. It just won't be different from the traditional harmony-centric Western musical model.

By the way, I studied CS and my full-time job is a Software Engineer. So I doubt our disagreement comes from my background in computer science.

You're misunderstanding what I'm saying. Music theory from other cultures are of course music theory as well. Each composer can (and almost always will) have their own idiosyncratic music theory as well. There is nothing contradictory here.

Also I'm a composer with extensive knowledge of how to make, orchestra, and mix acoustic or electronic music. This thread has an extreme Western bias, just because something is studied in a particular way from Western music theory perspective, it doesn't mean it has to be that way.

Check my comment here: https://news.ycombinator.com/threads?id=gnulinux#42368137

No you're simply wrong. This is how a "classical Western" musician thinks of music, but this is not necessarily what music is. Timbre is the main expressive content in many cultures.

Check my comment here: https://news.ycombinator.com/threads?id=gnulinux#42368137

This is exactly what I'm talking about. In Western music timbre is akin to fonts. You have a composition for piano, you play it, record it in MIDI, and reskin it with some other timbre in studio. This is an extremely Western way of looking at music. There are countless cultures where timbre is the "main" part of the music where the harmony and/or rhythm would be like fonts/reskins and timbre is the main juice composers and improvisers try to squeeze out. This type of distorted view on music is rooted in 18th/19th century beliefs of non-Western art being "primitive" art even though every single culture that's known to humanity have a unique musical tradition. This is an extremely anti-humanistic look at music.

Found the classically trained musician.

Any and all formal, mathematical, informal theory about music can be called music theory. Music theory is about modeling music. Period. It does not matter if it's about harmony, rhythm, pitch, form, timbre, dynamics, or some other aspect of music. Whether it helps with understanding music, composing music, improvising music etc is a separate topic. Music theory neither has to be about practical music making skills, nor it has to be about music of a particular artistic tradition. It just needs to present some model that can be a helpful tool in some musical context. Maybe what you call "audio engineering" is a specialized skill for some musical traditions, but for musical traditions where the expressive content primarily comes from timbre and synthesizers are common instruments, it will be an essential music making skill.

In the US, a random/personal selection of major works that will be public domain are:

* Ernest Hemingway's novel "A Farewell to Arms"

* Ludwig Wittgenstein's essay "Some Remarks on Logical Form"

* The first part of the 14th edition of Encyclopædia Britannica

* William Faulkner's novel "The Sound and the Fury"

* René Magritte's painting "The Treachery of Images"

* Wassily Kandinsky's painting "Upward"

* "Un chien Andalou", directed by Luis Bunuel and cowritten by Salvador Dali

* "The Cocoanuts", the first film of the Marx Brothers

* the first "Silly Symphony" cartoons, including "The Skeleton Dance".

Not a bad year at all!