enricozb

Make a habit of asking yourself around once an hour, “am I dreaming”, eventually (for me it took a week) this habit finds its way into a dream.

In case anyone is curious, the proof of LEM from AC is: Diaconescu's Theorem [0]

[0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....

In the vaguest sense possible. Dreams for me feel very concrete but definitely aren't. If I was debugging something in a dream and became lucid, and attempted to read the "code" on the screen, it would be impossible. Just a swirl of letter-like things that made no sense whatsoever.

This is a fair point. I usually only "jump" from directories that have at most 500k files, and the median is way closer to ~500 files.

Even in the worst cases, at least with my i7 NUC and using fd instead of find, it's less than 500ms to load the entire list into fzf.

Is there some functionality that `z` offers that fzf doesn't? I have a keybinding that essentially does `open $(fd | fzf)`, and that is how I go _anywhere_ in my file system. Completely changed how I use the shell.

I personally find that fzf is better because I can see where I'm going to end up before I accept the operation.

I think this is an important point to focus on when writing a new type-safe language. LEAN for example has a very impressive type system (honestly seems like magic sometimes), and clearly all of the "impossibility" is shoved into the computational complexity of the type-checker.

Despite the fact that some of the languages listed here have undecidable type systems, it doesn't feel like many common-purpose languages have purposefully gone down the undecidable route to bring some really cool type-safety.

This reminds me a lot of the WaveFunctionCollapse texture generation algorithm [0]. It "generates bitmaps that are locally similar to the input bitmap."

Very cool!

[0]: https://github.com/mxgmn/WaveFunctionCollapse

There can be parser considerations:

    a < b

can be greedily interpreted as a comparison, despite the next character being a >

    a [ b

can be greedily interpreted as accessing a field in a map, despite the next character being a ]

It may be easier to branch in one of those cases instead of the other.

Not at all familiar with the potential issues (if any) in go, but this is from experience in writing a few languages.

I personally don't like `curl | bash` because I don't know _how_ something will install: 1) What are all of the directories that something will insert itself into? 2) What of my files (.bashrc, etc.) will it modify? 3) If it modifies those things, will it tell me?

The `curl | bash` install pattern means that it can do _anything_.

Using a package manager I know that the install will be "typical", and easy to uninstall (that's the case with most of the package managers that I use anyways). Each package manager has a different pattern, sure, but at least it will be predictable.

Are there better arguments for anything in pure math being a posteriori? I fail to see how 4CT (or any mechanized/computer-aided proof) could possibly support this idea.

This makes much more sense. I thought that my brain was unconsciously interpreting the meaning of the arrows, which was completely unbelievable to me.

How else would you write that you want to match all strings that don't contain string X? If you were matching at a specific position, you should use a negative lookahead (?!xyz), but I think in some cases you might need the mess above.

I thought the message broadcasting and asynchronous behavior of Snap is really cool, specifically how sprites can have multiple code blocks each responding to messages or events.

I'm actually listening to a TEALS meeting right now! Funny to see it on HN.

This is cool. Gives some intuition as to how object files work.

I'm talking specifically about the function calls, which are effectively the same in C, Rust, Python, Lisp, Haskell, and many others. No matter how terse, it's always some form of

<name of function> <value1> <value2> <value3> ...

The absence/presence of parenthesis and commas don't add anything of semantic value here, so that's not really what I'm referring to.

The problem is, is that the values often don't have any meaning attached to them, especially when they are literals. C++ codebases are pretty bad about this with boolean parameters, just having a random `true` at the end of the function call.

Variable names at the call-site are good hints, but we often pass the same variable to different functions, and the name doesn't exactly fit the meaning of each function. This is why I think requiring named parameters, at least by default, is better.

They are biased to new readers of a codebase, not of a language, which is really just another way of saying that the code is very readable.

When giving an example on how infix notation reads better:

    // This is obviously not too right
    ",".splitBy("1,2,3,4,5")

    // This should be right, because it reads out more naturally
    "1,2,3,4,5".splitBy(",")

It's funny that in Python split works this way but join doesn't. This is because in the case of split both arguments are strings, but for join one of the arguments is a Sequence, which is a general protocol rather than a class.

The proposed solution by Keli is to be inspired by the Smalltalk-style message syntax:

    'Hello world' replace: 'Hello' with: 'Bye'

I think, in general, requiring named arguments is a good thing. Swift does it, and in codebases with a decent amount of TLC, it looks great.

Function calls are one of the weird places were the syntax of the language rarely helps you figure out what is going on, and for the most part is just a sequence of human-written names one after another, and in languages with custom operators it could be even terser.

In comparison, if-statements, loops, pattern matching, etc. were (hopefully) designed to be expressive. I think by requiring named arguments, function calls will also be much more readable, relying less on an active human effort to do so.

I believe another word for enums (in the Rust sense, not in the C++ or Java sense) are tagged unions.

How do I go from not understanding economics/finance, to pretending to understand it? I feel like that finance uniquely is a field that every time I have tried to penetrate I get a mix of unintelligible jargon and mathematics as a facade of rigor.

I am comfortable reading both math and programming textbooks, but every finance book I've picked up so far seems to quickly not make any sense to me at all.

Unsure if this works for the RM2

Drawing and marking up PDFs works really well, I do this with math textbooks frequently, but you're correct that the highlighting is nothing more than a "drawing" You can't go to the pages you've highlighted, or even extract text you've highlighted.

It's almost equivalent to being able to write directly on a textbook, however you can export your marked up document as a PDF.

What a cool resource. I've been meaning to finish an MVP for a programming language I've been trying to write, and it's pretty encouraging how many languages use undecidable type systems.

> it's here to stay

Would you be surprised if it just disappears in a year or two, like Vine, Orkut, Myspace, and other "giants" of their day did? I personally wouldn't because these things just come and go. I think it's really hard to make the claim that "it's here to stay".

minimalist != that login screen

This is what I figured would be the reason to remove comments, because they would hold some other non-human information. It's unfortunate that people do this. The main reason for comments for me would be for config files, which maybe shouldn't be in JSON anyways.

I wish JSON had 1) trailing commas 2) comments (I'm not sure if this is a good idea or not but every once in a while I impulsively write comments)

Those progress bars look delicious

Depends on who the paper is for. Theoretical CS papers for example, often don't have any code, but sometimes have pseudocode (for example in page 4 of PRIMES is in P [0]), to describe their algorithms. If the paper is written for people with less math background then writing up the algorithm in at least once language as a sample implementation is the way to go.

Also there's nothing wrong with doing both?

[0]: https://annals.math.princeton.edu/wp-content/uploads/annals-...

Have you ever read a perl program?

Since when does static typing imply monads...