enricozb

Replying in case anyone is in Amsterdam :)

Same, especially given how long that app specifically takes.

The NL Times just translates Dutch articles and editorializes them for a (mostly American) audience. They should be consistently taken with skepticism. In this case, as other commenters have pointed out, this is "just" Google Analytics.

Pretty neat! However, if you wanted to know the _probability_ of a noodle crossing any line in the long noodle case (L/W > 1), the expression is more complex (and I believe would require an integral) :).

It's interesting that the number of crossings is independent of whether L/W is less than or greater than 1, but the probability of crossings is equal to 2pi * L/W only in the short case. This makes sense since in the short case the noodle can at most cross a single line.

I believe the author is the creator of Bun.

Proof irrelevance I don't think is accepted in constructivist situations. Those are, however, not that relevant to the recent wave of AI math which uses Lean, whose type system includes classical mathematics.

I am excited for some alternative syntax to jq's. I haven't given much thought to how I'd write a new JSON query syntax if I were writing things from scratch, but I personally never found the jq syntax intuitive. Perhaps I haven't given it enough effort to learn properly.

What sorts of jobs, out of curiosity?

As a counterexample, the BBC financed the show that this sketch was from: https://www.youtube.com/watch?v=DuPBbFOiygo

What about it is incompatible with the EU?

Perhaps I overstated how related the two were. I was pulling mostly from the Lean documentation on Universes [0]

> The formal argument for this is known as Girard's Paradox. It is related to a better-known paradox known as Russell's Paradox, which was used to show that early versions of set theory were inconsistent. In these set theories, a set can be defined by a property.

[0]: https://lean-lang.org/functional_programming_in_lean/Functor...

Yes the type theoretic analog to Russel's (set theoretic) paradox is Girard's (as mentioned in the abstract) paradox.

I came across this when wondering if there were any efforts to give programmers additional information via audio, similar to how colors are used in syntax highlighting.

RDJ or Tatsuya Takahashi?

The final comments in this text seem sobering and indicate an openness to change. I worked recently on a project to migrate RediSearch to Rust, and this was partially motivated by a decent number of recent CVEs. If SQLite doesn't have this problem, then there needs to be some other strong argument for moving to Rust.

I also think it's important to have really solid understandings (which can take a few decades I imagine) to understand the bounds of what Rust is good at. For example, I personally think it's unclear how good Rust can be for GUI applications.

Today's usage from what edits I can recall:

- I wanted to edit the visibility (pub -> pub(crate)) of most but not all functions in a class.

- I changed a macro to not require commas in a list of items it took in as input.

- I changed a function to deal with utf-8 codepoints instead of bytes, so I wanted to rename all uses of "byte" to "char".

Basically, localized find and replace, with a bit of flexibility.

I think if the compiler determines that it can drop a 'static, because nothing uses it after a certain point, it may drop it.

It carries some weight, very roughly in the direction of formal verification. Since (assuming there isn't any unsafe), a specific class of bugs are guaranteed to not happen.

However, this repo seems like it uses quite a bit of unsafe, by their own admission.

This idea about communicating size/alignment is actually something we're doing on the port of RediSearch to Rust [0]. We have an "opaque sized type" which is declared on the Rust-side, and has its size & alignment communicated to the C-side via cbindgen. The C-side has no visibility into the fields, but it can still allocate it on the stack.

It's a bit ugly due to cbindgen not supporting const-generic expressions and macro-expansion being nightly-only. It seems like this will be a generally useful mechanism to be able to use values which are not traditionally FFI-safe across FFI boundaries.

[0]: https://github.com/RediSearch/RediSearch/blob/cfd364fa2a47eb...

It's kind of an exploratory phase for what works sensibly with Rust's borrow checker, especially since most UI libraries/frameworks really rely on a GC.

I used to make animations with https://pivotanimator.net/ a lot as a kid, trying to make fight scenes like these. A sort of related thing is ToriBash, which is kind of a multiplayer 3D animation game where you fight each other by making decisions on which muscles to contract at each time interval.

Loved this stuff so much. I miss my summers off from school, where I would never think of a day gone as time "spent".

When reading this project's wiki [0], it mentions that Kanal (another channel implementation) uses an optimization that "makes [the] async API not cancellation-safe". I wonder if this is the same / related issue to the recent HN thread on "future lock" [1]. I hadn't heard of this cancellation safety issue prior to that other HN thread.

[0]: https://github.com/frostyplanet/crossfire-rs/wiki#kanal [1]: https://news.ycombinator.com/item?id=45774086

Is this at all like vanadium? [0]

[0]: vanadium.github.io

What is coming/accelerating is the mental form of obesity, with very similar corporate interests and dynamics.

Huge fan of this sort of work, would like to put my DS to use someday.

Typst is great for web content as well (even though their HTML export functionality is still experimental). I've written blog posts on interaction nets in Typst [0] and I really like how the diagrams look.

[0]: https://ezb.io/thoughts/interaction_nets/lambda_calculus/202...

If it compiles, it typechecks. If it typechecks, the proof is correct. This is a consequence of the Curry-Howard correspondence [0].

From a pure mathematician's standpoint, the content of a proof is kind of (waving big hands here) irrelevant. It's more that the existence of a proof implies the theorem is true, and thus can be used to prove other theorems. Because of this "proof-irrelevance", a great foil to an LLM's propensity to hallucinate is something like Lean. In Lean, and in theorem provers oriented towards classical mathematics, the statement of the theorem being proved is what matters most. And due to Curry-Howard, the statement is equivalent to the signature/declaration of the function, which is what the human ought to verify, while Lean will verify the body.

[0]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon....

I did this [0] (gpt in rust) with picogpt, following the great blog by jaykmody [1].

[0]: https://github.com/enricozb/picogpt-rust [1]: https://jaykmody.com/blog/gpt-from-scratch/

I recently learned that macOS has a (by default) case insensitive filesystem. How does this line up with the certification?

When I say "how did we get here", I don't mean "how did we end up with these opinions (e.g. racism) on our soil". I mean something more like:

1. Why is discussing these things so difficult? So many internet forums are a pure deluge of unkindness, anger, and dishonest discussion.

2. There was a video of someone promoting their social media handle and asking people to subscribe with the backdrop of the shooting. How does someone end up acting like this?

I do not think there will be a time where racism is eradicated like a disease, but I think it's possible to confine it to small spaces and individuals. Similar to how I believe the majority of views like pedophelia: people with those mindsets exist, they don't form (huge) groups, and are generally consistently condemned. With the values I believe the US to have (tolerance of opinions and religion) this will always be a constant struggle.

Continuing with this disease analogy, the internet + social media has removed all possible herd immunity strategies to stupid ideas. People with any kind of ideology can search up their groups and commiserate, without ever encountering a differing viewpoint.

Furthermore, people are offloading their thoughts more and more to LLM's, so much so that we're becoming the mental equivalent of those wall-e humans [0].

We're not thinking for ourselves. Other people are thinking for us, delivering those thoughts to us, pre-digested. This leads to reactionary behavior, I think. And in an environment with such a reactionary populace, populism becomes so easy to exploit.

[0]: https://miro.medium.com/v2/resize:fit:1100/format:webp/1*uFK...

P.S. Sorry for the rambling. You're not wrong that the US has been, and still is, incredibly hostile to specifically identifiable groups of people. However, I think that the ability to discuss how to go about solving/remedying/containing this has been uniquely hampered in the last 20 years.