ww520 (u/ww520) - Readit News

ww520 commented on 450× Faster Joins with Index Condition Pushdown readyset.io/blog/optimizi... · Posted by u/marceloaltmann

futevolei · 10 hours ago

Do the db guys at your company help you optimize queries and table set up at all? Ours basically don’t at all. Their job is to maintain the db apparently and us devs are left to handle this and it seems wrong. I’ve been partitioning tables and creating indexes the past few weeks trying to speed up a view and running explain analyze and throwing the results in Gemini and my queries are still slow af. I had one sql class in college, it’s not my thing. Seems like if dbas would spend a few minutes with me asking about the data and what we are trying to do they could get this guys results relatively easily. Am I wrong?

ww520 · 9 hours ago

Nope. If they didn't actively work against us, we would thank the lucky stars.

ww520 commented on Project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover imperialcollegelondon.git... · Posted by u/ljlolel

frakt0x90 · 4 days ago

I know nothing about theorem provers. Is the idea that you can prove a large number of simpler statements that build on each other until it all implies the top level theorem you're proving (like how IRL math works)? That way you don't have to understand the gargantuan computer program all at once?

It just seems like it would be as hard to verify the accuracy of the code written to prove a complex theorem like FLT as a manuscript written in English. But if you can rely on smaller statements that build on each other, it would make more sense.

ww520 · 3 days ago

From the little I know of, language based provers like Lean allow mathematicians to specify the steps of a proof in a precise language format that can be “run” by a machine assisted prover to prove its validity. It automates the verification and makes proofs reproducible.

In the past when proofs were done by hands, little mistakes or little changes could lead to a complete failure of the proof. Mathematicians spent weeks or months to redo the steps and recheck every little detail.

Machine assisted prover basically raises the abstraction level for theorem proving. People don’t need sweat about little details and little changes in the proof steps.

Language based machine provers also enable wider corroboration as a problem can be subdivided into smaller problems and farmed out to different people to tackle, perhaps to different experts for different parts of the problem. Since everyone uses the same language, the machine can verify each part and the overall proof once the parts come together.

ww520 commented on Show HN: Building a web search engine from scratch with 3B neural embeddings blog.wilsonl.in/search-en... · Posted by u/wilsonzlin

ww520 · 11 days ago

Mad respect. This is an incredible project to pull together all these technologies. The crown jewel of a search engine is its ranking algorithm. I'm not sure how LLM is being used in this regard in here.

One effective old technique for ranking is to capture the search-to-click relationship by real users. It's basically the training data by human mapping the search terms they entered to the links they clicked. With just a few of clicks, the ranking relevance goes way up.

May be feeding the data into a neural net would help ranking. It becomes a classification problem - given these terms, which links have higher probabilities being clicked. More people clicking on a link for a term would strengthening the weights.

ww520 commented on A spellchecker used to be a major feat of software engineering (2008) prog21.dadgum.com/29.html... · Posted by u/Bogdanp

IshKebab · 12 days ago

I've also found a lot of this stuff is due to naysayers telling people that things can't be fixed (because really they don't want to bother). You need a strong leader to say "no it can and we will".

ww520 · 12 days ago

Or the incentive aligned.

ww520 commented on Faster substring search with SIMD in Zig aarol.dev/posts/zig-simd-... · Posted by u/todsacerdoti

burntsushi · 13 days ago

Another challenge may be as a result of using a portable SIMD API instead of specific ISA instructions. I'm specifically thinking about computing the mask, which on x86-64 is I assume implemented via movemask. But aarch64 lacks such an instruction, so you need to do other shenanigans for the best codegen: https://github.com/BurntSushi/memchr/blob/ceef3c921b5685847e...

ww520 · 13 days ago

A language level or std library level poly-fill for the missing SIMD operations for the platforms would be great.

ww520 commented on Faster substring search with SIMD in Zig aarol.dev/posts/zig-simd-... · Posted by u/todsacerdoti

ww520 · 13 days ago

Excellent write up. I really appreciate the clear and detailed explanation of the algorithm.

The nice thing about Zig’s SIMD operation is the register size support is transparent. You can just declare a 64-byte vector as the Block, and Zig would use an AVX256 or two AVX2 (32-byte) registers behind the scene. All other SIMD operations on the type are transparently done with regard to the registers when compiled to the targeted platform.

Even using two AVX2 registers for 64 bytes of data is a win due to instruction pipelining. Most CPU have multiple SIMD registers and the two 32-byte data chunks are independent. CPU can run them in parallel.

The next optimization is to line the data up at 64 byte alignment, to match the L1/L2 cache line size. Memory access is slow in general.

ww520 commented on Zig's Lovely Syntax matklad.github.io/2025/08... · Posted by u/Bogdanp

ww520 · 14 days ago

Zig is great. I have fun writing in it. But there’re a few things bug me.

- Difficult to return a value from a block. Rust treats the value of the last expression of a block as the return value of the block. Have to jump through hoops in Zig to do it with label.

- Unable to chain optional checks, e.g. a?.b?.c. Support for monadic types would be great so general chaining operations are supported.

- Lack of lambda support. Function blocks are already supported in a number of places, i.e. the for-loop block and the catch block.

ww520 commented on Windows XP Professional win32.run/... · Posted by u/pentagrama

ww520 · 16 days ago

Wow. This is very impressive. It would be trippy if IE can run https://win32.run again.

ww520 commented on Zig Error Patterns glfmn.io/posts/zig-error-... · Posted by u/Bogdanp

ww520 · 18 days ago

These are excellent tips. I especially like the debugger integration in build.zig. I used to grep the cache directory to find the exe. The integration avoids all the extra steps.

ww520 commented on OpenIPC: Open IP Camera Firmware openipc.org/à... · Posted by u/zakki

skywal_l · 20 days ago

I wonder if there is business in buying those cameras in bulk, flash them with thingio and resell them as "open" camera. Not sure if it's even legal. I guess flashing the camera probably void the warranty and the margin would be razor thin anyway.

ww520 · 20 days ago

It should be sold at a higher price. You perform a service by “unlocking” the camera.