#os #physics #raymarching
- Q-learning is not yet scalable
- found Todo.txt
    - from todo.txt tasks in my TRMNL
- #software
    - What is systems programming, really? (2018)
    - What Is Open Source?
        - learn about free v.s. open source
        - related
            - I feel open source has turned into two worlds
    - found is it really FOSS?
- #cg
    - On Shaping Light
    - watched Physics and Math of Shading
        - from SIGGRAPH 2025 Course: Physically Based Shading in Theory and Practice
    - Remaking Celeste's Lighting
- found Foundations of Computer Vision

#agent #blogging #compiler #context #formal #game #idea #interop #lean #news
- started using Mac's dictation in agent coding
- Blogging about papers
    - Design Patterns for Securing LLM Agents against Prompt Injections (on HN) (on lobste.rs)
        - "the writing is clear, it’s enjoyable to read and the target audience clearly includes practitioners, not just other researchers"
- #cg
    - Luxe Game Engine in preview now
        - 2D/3D, cross-platform (including web)
        - written in c++, scriptable with Wren or any language that can interact with C
        - optional editor to build worlds, animation, ui etc.
    - Voronoi, Hashing and OSL
        - found Open Shading Language (OSL)
            - was originally developed by Sony Pictures Imageworks for film animation and visual effects
            - has features such as radiance closures, BSDFs, and deferred ray tracing as first-class concepts
- Three Algorithms for YSH Syntax Highlighting
    - Coarse Parsing with regexes + a context stack could be even more accurate than Context-Free Parsing used by tree-sitter
    - recognizing most languages with Tree-sitter requires writing C code in an external scanner
- found Tattoy: a text-based terminal compositor (on HN) (on lobste.rs)
    - considerate design for text contrasts: "detect low contrast text and auto adjust the foreground colour within the constraints of your chosen terminal theme to find the nearest colour that meets a minimum contrast threshold"
    - usage example: terminal minimap, background video, shadertoy shaders
- #formalization
    - found Litex: Scale Formal Reasoning in AI Age
        - "Traditional proof assistants like Lean4 require learning hundreds of unfamiliar keywords and complex type theories. Litex enables formal verification with just 8 intuitive keywords (forall, exist, not, or, fn, prop, obj, set) and familiar Python/Go-like syntax"
    - 100 years of Zermelo's axiom of choice: What was the problem with it? (2006) (partially formalized in Agda)
- #datalog
    - Implementing Logic Programming with Prolog and Datlog
    - Datalog in Rust
- #rust
    - OxCaml, Jane Street's extension of OCaml is now open-source (on HN) (on lobste.rs)
    - Hypershell: A Type-Level DSL for Shell-Scripting in Rust powered by Context-Generic Programming
    - Datalog in Minikanren (on HN, many good references about datalog, and scheme)
    - Bzip2 crate switches from C to 100% Rust
        - `c2rust`, crate cc, `miri`
        - `cargo fuzz`, `cargo audit`, `semgrep` (particularly semgrep-rules)
- #zig
    - watched Writing polymorphic code (anytype, comptime interface, tagged union)
        - found Zimpl (why)
        - tagged union example with `inline else`
    - Compiler optimization options - memchr and ripmemchr case study
    - C2y: Hitting the Ground Running
    - GCC, glibc, stack unwinding and relocations – A war story
    - The Art Of Packing Data
- #apl
    - APL Style: Patterns/Anti-patterns
    - Solving LinkedIn Queens with APL
    - Klong: A Simple Array Language
    - Coding in Advent in BQN
    - apl87
    - My Ideal Array Language (on HN) (on lobste.rs)
        - APL, Mojo, MLIR BQN etc., but no mention of Julia
        - this comment recommend Astropy and much more
    - BobMcDear/trap: Autoregressive transformers in APL #lm
- Introducing Sulka, the Hardened Yocto Distro
    - learn about the possibility to maintain a distro by a single person
    - the Yocto project provides toolkits to create custom Linux distributions, especially for embedded systems
    - Sulka is a hardened Poky, and there are alternatives like Welma
- #ai
    - To fuel AI, US Congress moves to fast-track nuclear plant approvals
    - The Emperor's New LLM
    - Builder.ai did not "fake AI with 700 engineers"
    - Self-Adapting Language Models
    - Resa: Transparent Reasoning Models via SAEs
    - Simulink (Matlab) Copilot
    - Rethinking Losses for Diffusion Bridge Samplers
- #quantum
    - Quantum Computing without the Linear Algebra
    - Geometry from Quantum Temporal Correlations
- news
    - Apple's Liquid Glass is prep work for AR interfaces, not just a design refresh
    - Next.js 15.1+ is unusable outside of Vercel
    - The European public DNS that makes your Internet safer
- general
    - Feedback Is Not an Attack
    - Ask HN: How do I give back to people helped me when I was young and had nothing?
        - "Focus less on those who helped you, and more on helping others."
    - am i too self-aware?
    - When random people give money to random other people (2017)
    - We Live In a Golden Age of Interoperability
    - No Hello
- #biology
    - Sperm are very different from all other cells
    - The Ecosystem Dynamics That Can Make or Break an Invasion
    - When we die do we still have any of the original cells from our birth?
- found Modularizing George Cave's eInk Energy Dashboard
    - could be used to make widgets for various devices
- found Radicle Desktop: a graphical user interface for the Radicle peer-to-peer code forge
    - learn about Radicle, a sovereign code forge built on Git
- found Qrkey – Offline private key backup on paper
    - not sure if it's a good idea security-wise, but neat anyway

#benchmark #formal #lean #news #os #rss #rust #tui #z3 #zig
- Solving LinkedIn Queens with SMT
    - in Z3 SMT solver instead of CVC5 SMT solver as in Using SAT to Get the World Record on LinkedIn's Queens
    -  SAT solvers are "criminally underused by the industry" (from Modern SAT solvers: fast, neat and underused)
    - SMT solvers are "higher-level" than SAT, capable of handling more data types than just boolean variables
    - It's a lot easier to solve the problem at the SMT level than at the SAT level
    - people prefer SMT to SAT
    - Glucose, an SAT solver is really fast
    - The Hat, the Spectre and SAT Solvers (2024) (on HN) (on lobste.rs)
- jemalloc Postmortem
    - they "reached a sad end for jemalloc in the hands of Facebook/Meta even though most of the people involved were acting in good faith"
    - "the root of the problem is lack of awareness about external uses and needs"
        - even "unaware of its replacement until after the fact"
    - "internally siloed open source projects cannot thrive"
    - should evaluate alternatives
        - TCMalloc by Google (with Bazel painpoint)
        - mimalloc
            - adopted by CPython 3.12: "it is fast, thread-safe, and NUMA-aware"
        - StarMalloc: verified memory allocator
        - phkmalloc
- looking for best way to read Hacker News comments
    - most TUI are not working well for reading comments, see `just prep-hkt`
    - found Vue HN that supports dark theme, and groups comments, it works pretty well with Doubao auto-translation
    - found Hacker News RSS and chose the front page feed, and I have already subscribed to the best comments feed
- Could an LLM create a full Domain-Specific Language?
    - rather complete methodology for creating a DSL
    - code: jcabot/funding-dsl
- The last six months in LLMs, illustrated by pelicans on bicycles
    - an interesting benchmark for LLMs
- #ai-safety #env
    - AI Boom Drives 150% Surge in Indirect Emissions at Major Tech Firms, UN Warns
        - numbers for the environmental impact of LLMs
        - related
            - AI threatens to raid the water reserves of Europe's driest regions
    - Environmental Impacts of Artificial Intelligence
    - Mistral reports on the environmental impact of LLMs (on HN)
        - Simon Willison | Our contribution to a global environmental standard for AI
    - Problems the AI industry is not addressing adequately
    - Generative AI’s crippling and widespread failure to induce robust models of the world
- Type-based vs Value-based Reflection
    - value-based (C++26)
        - "while we have new syntax for getting into (`^^e`) and out of (`[: e :]`) the value domain, once you’re in the value domain — it’s nice to just stay there"
        - "C++26 reflection does bring with it new syntax and a bunch of new semantics. But the benefit is that a lot of metaprogramming starts to look more like regular programming. There is a lot less syntax in the implementation side of things. "
    - type-based (Reflection TS published in March, 2020)
    - wondering the Zig equivalent
    - Discover C++26’s compile-time reflection
    - C++26 Reflections adventures and compile-time UML
- Reflections on Sudoku, Or the Impossibility of Systematizing Thought
    - limitation of TDD
        - tests don't fix the underlying issue of "knowing what to do"
    - alternative approach by Peter Norvig
        - analyzing the high-level problem and then breaking down the data structures and outlining the solution in the course of ~20 lines of code
- found A Lightweight Merge Queue using GitHub Actions
- Rumour: Google intends to discontinue the Android Open Source Project
- A tale of two spacetimes
- In case of emergency, break glass
- skimmed Patterns for Modeling Overlapping Variant Data in Rust
- What I talk about when I talk about IRs

#cg #compiler #diagram #formal #game #optimization #os #proof #render #rust
- wrote Trying Zig's self-hosted x86 backend on Apple Silicon (on reddit)
- #lean
    - Premise Selection for a Lean Hammer
        - the paper behind LeanHammer
    - Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
    - Trinity: an autoformalization system for verified superintelligence
    - Mathesis: Towards Formal Theorem Proving from Natural Languages
    - watched Mr. Mario Carneiro | Lean Meta-theory: The Proofs behind the Proofs
- Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library
    - used Aeneas, a Verification Framework for Rust that supports F*, Coq, HOL4 and Lean
        - the team also built
            - Charon to extract information from rustc internals for semantic analysis thus verification
            - Eurydice, a Rust-to-C compiler to provide a backwards-compatibility story as the verification ecosystem gradually transitions to Rust
    - used Revizor - a fuzzer to search for microarchitectural leaks in CPUs
        - analyze binary code for specific compilers and platforms
        - find side channel vulnerabilities caused by timing leaks or speculative execution
        - which aren't visible in the source code
        - for today’s CPUs, every new optimization may open a new side channel, which renders constant-time programming insufficient
- found Lightweight Diagramming for Lightweight Formal Methods
    - formal methods help users define, explore, verify, and diagnose specifications for complex systems incrementally
    - Forge: A Tool and Language for Teaching Formal Methods
        - similar to Alloy 6
        - uses Sterling visualizer
    - Cope and Drag (CnD)
        - embedded in an open-source visualizer for Forge
        - focuses on encoding the spatial intuitions implicit in communicating the model
            - constraining spatial layout (such as positioning child nodes below their parents in a binary tree)
            - grouping elements (like clustering related components in a software architecture)
            - directing drawing style (for instance, coloring nodes in a red-black tree based on their color)
- #debugger
    - strace tips for better debugging
    - Demystifying Debuggers (a series)
    - Linus on Why Debuggers Are Actually Bad For Developers
    - found Building a Debugger: Write a Native x64 Debugger From Scratch
- #raku
    - Raku's "core"
    - Raku's FAQ
    - RakuAST: a foundation for Raku macros
    - Raku in y minutes
- Readings shared June 10, 2025
- realized that Pocoo is behind Sphinx, Jinja, Pygments etc.
- found Verse Language, a new scripting language for Fortnite by Epic

#agent #os #render #tui #typst #web #zig
- My Unfiltered Take on the AI Coding Agent Landscape
    - found and tried amp
        - love their Frequently Ignored Feedback but disagree with some of them
        - it gives me an addictive experience, but it's quite costly and the price model is not very transparent
    - found YouWare and would love to try more
- Zig-style generics are not well-suited for most languages (2022)
- Ratatui - Are We Embedded Yet? (#2)
    - learn about Mousefood, a embedded-graphics backend for Ratatui
- found Quarkdown - Markdown with superpowers
    - interesting but it's a little late to the party now that we have pandoc and quarto
    - the syntax and scripting looks good
    - its PDF output is based on rendering web pages, a big no-no for me, as I need LaTeX-level professional typesetting like Typst has
- #css
    - Partial Keyframes
        - neat CSS animation trick
    - More Frontend Web Tricks
    - Color Everything in CSS
    - Printing the web: making webpages look good on paper
    - HUG CSS, how I approach CSS architecture
    - What Does `playsinline` Mean in Web Video? | CSS-Tricks

#agent #compiler #diagram #formal #llvm #makefile #news #optimization #rust #sec
- Lightweight Diagramming for Lightweight Formal Methods
- #perf
    - Why doesn’t Rust care more about compiler performance?
    - One Law to Rule All Code Optimizations
    - Simulating Time With Square-Root Space
    - Is Rust faster than C?
    - Revisiting Knuth’s “Premature Optimization” Paper
- #os
    - Asterinas: A Linux ABI-compatible, Rust-based framekernel OS #rust
        - framekernel: the performance of a monolithic kernel and the security of a microkernel
        - OSTD, an OS framework, so that a Hello World kernel in 100 lines of safe Rust
        - TCB (Trusted Computing Base) is the minimal unsafe code required to build a kernel in safe Rust
            - ~15K LOC, 14- rich OS features
        - aims to verify unsafe code with Verus
        - uses model checking with Converos to uncover hard-to-find concurrency bugs
        - see also Asterinas: a new Linux-compatible kernel project
    - Blog series on creating an OS in Rust (on HN) #rust
    - Starina - A modern general-purpose microkernel OS
        - from Building Linux kernel on macOS natively (on HN)
            - Clang Built Linux effort helped to build Linux kernel with clang + LLVM instead of GCC + GNU
            - it seems to work and is simple enough, I should try it sometimes
    - Munal OS: A graphical experimental OS with WASM sandboxing
        - written in Rust
        - embeds wasmi
        - no virtual address space as userspace is inside WASM sandbox
        - only VirtIO so it runs only in an VM
        - has links to OS dev resources
    - Talos: a container optimized Linux distro, which is declarative, immutable, secure
        - minimal: consists of only a handful of binaries and shared libraries: just enough to run containerd and a small set of system services
            - written in Go
        - no SSH and console access, fully controlled by API via gRPC
        - Which Kubernetes is the Smallest? Examining Talos Linux, K3s, K0s, and More
            - Talos has the minimal footprint
    - The high-level OS challenge
    - A DOS-like hobby OS written in Rust and x86 assembly
        - RoureXOS rewritten in Rust
    - Tilck: A Tiny Linux-Compatible Kernel (on HN)
- Makefile.md - Possibly Use(ful|less) Polyglot Synthesis of Makefile and Markdown
- comments on Qwen3 embedding models
- #prolog
    - from Readings shared June 9, 2025
    - Teaching and learning mathematics with Prolog
    - Exploring Topological Spaces with Prolog: A Practical Approach Using “Mathematics with Prolog”

#agent #datafusion #docker #duckdb #elixir #formal #harbor #idea #json #lemmy
- #selfhost
    - Ditching HAProxy (in my homelab)
        - found Ran out of infrastructure titles from the author
            - backrest
                - for using `restic` to manage backup repos and plans
                - tested that `restore` and `mount` work, as well as encryption and compression
                    - see also Running Veracrypt in Docker
                        - `--privileged`, `-m=nokernelcrypto`, locale etc.
                - supports monitoring via Healthchecks if backup jobs don't "check in"
                - a sec review: restic cryptography
            - MetalLB, a load-balancer implementation for bare metal Kubernetes clusters
            - `Talos`, moved to 2025-W24 › 🔗 › 2025-06-10
            - Unbound: a powerful validating, recursive, caching DNS resolver
                - could be used for home network
            - Salt with its GUI
                - is similar to Ansible, in the sense you use YAML to specify a state, but has a differening architecture, opting for a master/minion setup rather than Ansible's agentless SSH connections to each node
            - Apt-Cacher NG for caching apt packages
            - Harbor for caching container images
            - Headscale: self-hosted implementation of the Tailscale control server
            - Pocket ID for authenticate users with their passkeys
- #fediverse
    -Two Approaches to Solving the “Quiet Fediverse” Problem: Conversation Backfilling Mechanisms
    - The fediverse, explained
        - Lemmy
        - Pixelfed
        - BookWyrm
        - PeerTube
    - Pleroma: a lightweight federated social networking server powered by Elixir and PostgreSQL
        - from What Is Pleroma?
    - From Fediverse to Creating Personal Digital Space with Memos
        - Single-user Mastodon Instance is a Bad Idea
    - jakeg -> notes -> fediverse
    - ActivityPods: Personal data spaces powered with ActivityPub
    - tried matrix again and found a good TUI: iamb
    - Threads is adding Fediverse content to social feeds
- wish to test x86 on ARM Mac
    - due to Zig's self-hosted x86 backend is now default in Debug mode
    - found Intel-on-ARM and ARM-on-Intel with lima
    - container: tool for creating and running Linux containers using lightweight virtual machines on a Mac
- AI at Amazon: a case study of brittleness
    - that's how things got stuck in a big org, or at least slowed down enought to suffocate innovation
        - Decompensation: a service fall over after receiving a spike in external requests, mostly due to hierarchical decision-making
        - Working at cross-purposes: introduced an almost Darwinian flavor to org dynamics where teams scrambled to get their work done to avoid getting reorged and subsumed into a competing team
        - Getting stuck in outdated behaviors: had to constantly justify our existence and massage our projects with metrics that could be seen as more customer-facing
- Thank You, DataFusion: Queries in Rust, Without the Pain
    - SQL as a library, not a service
    - own your storage, your execution model, your schema, your optimizer
    - offers [SQL] and [Dataframe] APIs, excellent performance, built-in support for CSV, Parquet, JSON, and Avro
    - paper: Apache Arrow DataFusion: A Fast, Embeddable, Modular Analytic Query Engine
    - should take a deep look into DuckDB
- found Black Hat Zig: Zig for offensive security.
- Training a Rust 1.5B Coder LM with Reinforcement Learning (GRPO) | Oxen.ai