Programming

Explores how the Lean programming language handles 2 + 2 = 4, which other programming languages collapse into a bool, but Lean considers a Proposition, and requires Proof.

How does provably correct programming look? This article seems to give a good introduction and example.

Mono appears to be dead. I enjoy making life hard so I dont use windows. I am trying to learn very simple c# but am having trouble gettung visual studio to run anything on linux (debian/mint). It wont even run with dotnet in the terminal either. I dont really like all the features in vs either, i just want simple.

For reference im learning with the yellow book by rob miles. I want to learn the old way, not using a bunch of shiny helping tools (i never feel i really learn with those and it stunts my growth).

I've seen a few articles saying that instead of hating AI, the real quiet programmers young and old are loving it and have a renewed sense of purpose coding with llm helpers (this article was also hating on ed zitiron, which makes sense why it would).

Is this total bullshit? I have to admit, even though it makes me ill, I've used llms a few times to help me learn simple code syntax quickly (im and absolute noob who's wanted my whole life to learn code but cant grasp it very well). But yes, a lot of time its wrong.

Related discussion:

• https://news.ycombinator.com/item?id=44902127

I'm hoping to get pointed in the right direction on finding or creating a tool that can optimize the storage of items based on their dimensions and the dimensions of storage spaces available. Luckily there is only 1 dimension to measure (Width), so the constraints and logic are fairly simple (no 3D stacking needed).

In very rough terms, there will be 2 tables with the following fields: Table 1: Storage Space

• Storage ID: Unique ID for the space
• Storage Width: Numerical value in metres
• Storage Capacity: Numerical how many items can be stored side by side - generally 1 or 2.

Table 2: Storage Items

• Item ID: Unique ID for the item being stored
• Item Width: Numerical value in Metres

The optimization exercise is to run through the list of Storage Items and assign them to a Storage Space while minimizing the unallocated storage width (i.e. pack these items as tight as it can) while respecting that a Storage Space may have a maximum capacity of 1 or 2 items.

I'm not the coding sort myself (I can work my way around programming logic but I'm not immersed in it and it will take me a good deal of time) so I'm wondering if anyone may be familiar with tools that could hand hold analyzing data sets in this way, or ready-made solutions that happen to tackle the optimization problem.

Thanks in advance!

I just used this to update 600 lines, across 33 files! It worked great!

• In a separate memo, Microsoft CoreAI head Jay Parikh outlined a new structure that will see GitHub leadership reporting to several Microsoft executives.
• Microsoft developer division head Julia Liuson will oversee GitHub's revenue, engineering and support.
• GitHub chief product offer Mario Rodriguez will report to Microsoft AI platform VP Asha Sharma.

Rust 1.89 is now released, expanding x86 and x86/x86_64 platform support with new processor instructions and features, including additional AVX-512 intrinsics. The target_feature attribute adds support for SHA512, SM3, SM4, KL, and WIDEKL, giving developers better access to modern CPU capabilities directly from Rust code.

Full changelog: https://blog.rust-lang.org/2025/08/07/Rust-1.89.0/

cross-posted from: https://programming.dev/post/35278281

Hi everyone, I recently created an in-memory cache in Rust called PaperCache. It's the first in-memory cache that's able to switch between any eviction policy at runtime, allowing it to reduce its miss ratio by adapting to changing workloads. Currently, it supports the following eviction policies:

• LFU
• FIFO
• CLOCK
• SIEVE
• LRU
• MRU
• 2Q
• ARC
• S3-FIFO

It typically has lower tail latencies than Redis (though with the trade-off of higher memory overhead as it needs to maintain extra metadata to be able to switch between policies at runtime).

Feel free to check out the website (https://papercache.io/) which has documentation, a high-level article I wrote on Kudos (https://link.growkudos.com/1f039cqaqrk), or the paper from HotStorage'25 (https://dl.acm.org/doi/abs/10.1145/3736548.3737836)

Here's a direct link to the cache internals: https://github.com/PaperCache/paper-cache

In case you want to test it out, you can find installation instructions here: https://papercache.io/guide/getting-started/installation

There are clients for most of the popular programming languages (https://papercache.io/guide/usage/clients), though some may be a little unpolished (I mainly use the Rust client for my own work, so that one is kept up-to-date).

If you have any feedback, please let me know!

I'm wondering if you use any (graphical) clients to manage your Git, and if so, what client you use.

I myself have to use git professionally across all 3 major OS-es, and I currently use Sourcetree on Windows and macOS, and the Git tools built-in into IntelliJ on Linux.

Have given MaGit a try, but just couldn't get all the shortcuts to stick in my mind.

Interested to hear your experiences!

Archive: https://archive.ph/2025.08.06-191943/https://www.quantamagazine.org/new-method-is-the-fastest-way-to-find-the-best-routes-20250806/

If you were designing a standard library of a high level language (like Rust, C++, etc.) what would it do if while getting the current time of day (e.g. SystemTime::now()) it encountered a failed kernel system call (e.g. to clock_gettime) and why?

What do you think the existing implementations do?

• Return error or raise exception
• Return 0
• Return undefined values (like stack garbage)
• Panic/crash/segfault

I've been trying to make an RNG that outputs data in a way that has an entropy that approaches a user defined value as the output gets arbitrarily long. I've been struggling at a certain point that I'll detail later, but the main motivation for this project is just trying to practice on a problem like this. Here's my repo.

In this post, we'll be talking about Shannon entropy. Here's a good refresher for it. If you scroll down there's examples and the equation.

Looking at the equation, when developing this algorithm we have two different input values for it: the target entropy and the number of outcomes, n. From there, we can create a probability vector of length n whose entropy is equal to the target entropy, then we can map objects to elements of the probability vector and sample indices from the vector by using the alias sampling method. From there, we have a nice algorithm for creating sequences of any type that have the target entropy.

So where's the problem? It's in actually generating the probability vector. In order to get to a V0, I implemented two functions: helpers::compute_probabilities and helpers::find_lambda. compute_probabilities creates the probability vector that has the target entropy by sampling from the exponential distribution. find_lambda repeatedly calls compute_probabilities using binary search to converge on a lambda that produces a probability vector with the target entropy. The problem line is right here:

    pub fn compute_probabilities(num_outcomes: usize, lambda: f64) -> Vec<f64> {
        let unnormalized: Vec<f64> = (1..=num_outcomes)
            .map(|i| (-lambda * i as f64).exp())
            .collect();

When calculating the actual probability values, they get exponentially smaller as the probability vector gets bigger. This works. Technically. But in the worst way. When sampling using vectors generated using this function, they realistically only sample the first few elements. That's the problem. I want to more equally distribute the probability in such a way that doesn't make the tenth value arbitrarily small but the first value really large in comparison. For reference, using this function and lambda=1, the tenth element in the vector is 5x10^-5 but the first value .37.

I figured I'd post this before I start throwing a bunch of different distributions at this function to see if anyone sees any inherent flaws with my process.

@programming Unpopular opinion: 95% percent of all modern programming langueges are either bloated/proprietary/unneccesarily complex. pretty sure C & assembly can do it all (even for web development, just compile c to WebAssembly)

I want clean history, but that really means (a) clean and (b) history.

People can (and probably should) rebase their private trees (their own work). That's a cleanup. But never other peoples code. That's a "destroy history"

So the history part is fairly easy. There's only one major rule, and one minor clarification:

• You must never EVER destroy other peoples history. You must not rebase commits other people did.

[...]

If you are working with git together with other people, it's worth a read.

I think it's very interesting, and something i've been looking for for a very long time. Finally a programming language focused on efficiency

However, there are some important features that WinSock just doesn’t expose. […]

Rust’s current async ecosystem is built atop a particularly cursed concept. It’s an unstable, undocumented Windows feature. It’s the lynchpin of not only the Rust ecosystem, but the JavaScript one as well. It’s controversial. It’s efficient. […] Without it, it’s unlikely that the async ecosystem would exist in its current form. It’s called \Device\Afd, and I’m tired of no one talking about it.

“Jujutsu (jj) is a version control system with a significantly simplified mental model and command-line interface compared to Git, without sacrificing expressibility or power (in fact, you could argue Jujutsu is more powerful). Stacked-diff workflows, seamless rebases, and ephemeral revisions are all natural with jj [...]”

Part 2 of the series is out and is here.