ducktective

Basically, LLMs have reduced the incentives in doing open source.

If you go with agentic route, randos with money to spare on latest models, beat you. If you go LLM-free, AI corpos say "all the better for us! More free untainted dataset!"

"air-gapped" how?

It's often suggested that Lean is a general programming language but I don't see typical libraries to do basic stuff in it, like an arg parser, web server, GUI, SQL integrations etc.

Can lean generate small static binaries the same way Go/Rust/C/C++ can?

How practical is rewriting, say, grep in Lean?

- Is it possible to train only on math and logic materials and expect the model's response in math questions to be superior to general models with the same training/inference compute hardware?

- Are there non-LLM approaches to the above task with the goal of achieving a non-hallucinatory agent?

A question to those active in chip design industry: Are formal methods and formally proving a design more prevalent and normal in this industry compared to general software development?

Like for a Arm microcontroller design, do engineers thoroughly test and formally prove the correct functionality of every component? If that's the case, why silicon errata is a thing?

>distillation datasets

You ask about distillation but I wonder, is there any training datasets (~ TB-order) available that startup folks in SV use or is it so that everyone has to create their own scraping pipeline ?

Don't worry, AI's gonna fix it in Rust in Windows 12

You're doing something serious aaand suddenly out of nowhere the fan starts screaming cause some cryptically named process decides right now is the time to get stuck in some loop

>outdated

What modern features are you looking for in a say, document editor? My experience with LibreOffice Writer and Calc has been excellent. I'm happy there is no modern AI or cloud integration noise or ribbon bars with excessive whitespaces.

For starters, universities and government offices should not expect a proprietary format. Everyone should accept OpenDocument Format (ODF) or a similar FOSS format. MS Office, LibreOffice, OpenOffice and whatnot can compete in editing and rendering open formats.

Come to think of it, this is a good proposal for EU, thanks for the USB-C, by the way :)

Tangential, but does anyone know why in 2026 and on Debian 13, my machine still hangs when some process exhausts RAM?

Is there really no higher-priority kernel process to prevent total freeze of the system and send a SIGKILL to the culprit process when such a scenario happens?

My point was, people block js of websites by default. Why? Cause website devs abuse js and don't exclusively use it for basic interactivity of stuff like sorting table columns.

There is an incentive to use HTML for common interactivity purposes.

>single, simple JS file

It's all fine and dandy until marketing bros decide to shove all kinds of shady modals into that JS file. The JS side is not exclusive to trivial interactivity.

> including isolated testing environments

Given the attack vector having possible super-human capability, I'm not sure such an environment exists. "Isolated" according to who?

Maybe seL4 could be a viable option here...

>Do you think Japan and the EU would be better off if our/their economies were centred around trillion dollar companies that make a product that is 20% better than the Chinese models at 1000x the cost?

Why Japan and Europe don't develop a model that is 20% worse at 0.001x the cost?