#formal #haskell #lean #ocaml #os #rust #zig
- Having your compile-time cake and eating it too
    - Hindley-Milner (HM), the most popular human-friendly type system, used in Swift, Rust, Scala, Haskell, OCaml etc.
    - proposed four big features to replace pretty much all Rust macros, including derive ones, while keeping Rust's type system, and achieving (most of) Zig's comptime features
        - `@` or `@=`
        - `Abstract`
        - `TypeInfo` and `Field`
        - `Code` and `parse`
- CAPTCHAs don't work any more for ticket sellers
- Concepts vs type traits
- tachy0n: The last 0day jailbreak
- found Domain Theory Lecture Notes
- generate and read the following DeepWiki:
    - ymndoseijin/zilliam
    - ShabbirHasan1/unsynn
    - AstatineAi/ocaml-forester
    - pygae/galgebra
    - utensil/forest
- use GenSpark to generate Follow-up Research after Formalizing Geometric Algebra in Lean
- Does gratitude increase happiness?

#agent #apl #cg #compiler #git #haskell #lean #os #rust #software
- Anthropic’s ‘System Card’ for Claude 4 (Opus and Sonnet)
    - particularly fun reading
        - 4.1.1.1 Continuations of self-exfiltration attempts
        - 4.1.1.2 Opportunistic blackmail
        - 4.1.1.3 Self-exfiltration under extreme circumstances
        - 4.1.3 Excessive compliance with harmful system-prompt instructions
            - "mistakenly omitted the only finetuning dataset that included harmful system prompts"
- Forgotten APL Influences (2016)
- learn about Glean
    - a system for collecting, deriving and querying facts about source code
    - from Indexing Hackage: Glean vs. hiedb
- Pain in the dots
    - different semantics of two and three dot notation for `git log` and `git diff`
- Make Your Phone Grayscale
    - I've already started the practice, combining it with all-day nightshift mode
- The GCC compiler backend can now fully bootstrap the Rust compiler

#ocaml #os #rust #tla
- Why I love OCaml
- How to Get Your Research Paper Accepted
- Fork Union: Beyond OpenMP in C++ and Rust?
- #lang
    - Wren, a small, fast, class-based concurrent scripting language
        - "Think Smalltalk in a Lua-sized package with a dash of Erlang and wrapped up in a familiar, modern syntax."
        - Talon: Write Raylib programs in Wren
    - Picat, a rule-based language, in which predicates, functions, and actors are defined with pattern-matching rules
        - from Finding hard 24 puzzles with planner programming
            - "the only language that I know has a built-in planner module"
    - Dark, a serverless backend language
        - Darklang Goes Open Source
        - Goodbye Dark Inc. - Hello Darklang Inc
    - Roto
        - from Introducing Roto: A Compiled Scripting Language for Rust
    - Janet #lisp
        - a more batteries-included Lua, with Lisp/Clojure-inspired syntax
        - see The smallest embeddable scripting language, part 1
        - PEGs in a PEG
        - JNJ: J iN Janet
        - Bagatto, a static site generator written in Janet
    - goal, embeddable scripting array language
    - lamber, functional scripting language compiling to Lambda Calculus
- found many papers, see some HF papers worth skimming

#context #formal #idea #os
- Adventures in Symbolic Algebra with Model Context Protocol
    - maybe I should create MCP for GAlgebra
    - followup: Interfacing MCP with Combinatorial, Convex, and SMT Solvers
- Transpiler is a meaningless word (2023)
    - maybe that means I should give up on the idea that I could build a Forester transpiler
- found Obsidian Bases

#os #sqlite
- If composers were hackers
- found Litestream: Revamped, making SQLite apps reliably recoverable from object storage
- The Ingredients of a Productive Monorepo

#gpu #news #os #web
- Not causal chains, but interactions and adaptations
    - RCA(root cause analysis) model v.s. RE(resilience engineering) model, for incidents
    - related
        - The same incident never happens twice, but the patterns recur over and over
        - Quick takes on the GCP public incident write-up
            - “What went well” is more than just a pat on the back
            - Behind the scenes: Redpanda Cloud’s response to the GCP outage (on HN) (on lobste.rs)
        - Implicit is better than explicit
- Open Source Can't Coordinate
- Particle Life simulation in browser using WebGPU

#agent #docker #lemmy #mastodon #os
- Agent Recursion
- Semgrep: AutoFixes using LLMs
    - found a few alternatives to `semgrep`, e.g. ast-grep
- Adding Mastodon Comments to your Blog
    - Mastodon as comment system for your static blog
    - My blog now has Lemmy comments
    - learn about Glasp: Highlight the Internet & Build Your AI Clone
- async/await versus the Calloop Model
- Mimalloc Cigarette: Losing one week of my life catching a memory leak
- Ditching Obsidian and building my own
- found Qwen3 Technical Report
- found TestDesiderata
- found macOS VMs in a Docker Container

#apl #compiler #game #gpu #os #physics #quantum #shader #zig
- found Algorithms by Jeff Erickson (2019)
- Comparing parallel functional array languages: Programming and performance[van2025comparing]
    - learned that APL can run on GPU via Dyalog, the paper even discussed a flash attention implementation
    - BQN doesn't seem to run on GPU
    - it might be interesting to use arrayfire C API, even on Mac
    - prefer tilelang to DaCe
- found A JavaScript library for building parsers, interpreters, compilers, and more
- Layers All The Way Down: The Untold Story of Shader Compilation
    - introduces the motivation behind MojoShader, from Direct3D HLSL bytecode or assembly source to other shader languages
- found Mystical, a programming language that resembled magical circles
- Bare Metal Zig (2023)
- Google Scholar is manipulatable
- found Path Integrals in Quantum Mechanics, Statistics, Polymer Physics, and Financial Markets by Hagen Kleinert

#elixir #game #ocaml #os #rust #software #web #zig
- Parallel Scaling Law for Language Models
- #lang
    - The Language That Never Was
        - Leaving Rust gamedev after 3 years
        - Mun
        - jank
        - The Little Book of Rust Macros
        - MonoGame
- #rust/error
    - Using unwrap() in Rust is Okay
        - anyhow for applications and thiserror for libraries
    - On Error Handling in Rust
        - error_set, inspired by Zig's error set
        - snafu
- found GNU Parallel Examples
- found Lua for Elixir
- found OCaml Web Development: Essential Tools and Libraries in 2025
- found Teal: a statically-typed dialect of Lua, a statically-typed dialect of Lua

#formal #game #news #os #rust #tla #zig
- I don’t like NumPy
    - Writing a better code with pytorch and einops
    - Einops and Einsum Summarized
- looking for Zig way to implement eiops
    - Interesting (mis-)use cases for comptime
        - zig-infix-parser
    - Zig Comptime is amazing
        - ZEIN, Zig-based implementation of general-rank tensors
        - Functional Programming in Zig
        - What is Zig's Comptime?
        - comath: comptime math, used by zilliam
        - alg, Algebra for Zig
        - mecha, A parser combinator library for Zig
            - from Zig, Parser Combinators - and Why They're Awesome
        - parcom, see also this blog post
    - einops in Rust, with only backend `tch`
    - Einsums and einops-cpp are in C++
- The current state of TLA⁺ development
    - found Spectacle and tlafmt
- 10 Years of Stable Rust: An Infrastructure Story
    - formal methods projects built on Rust
- Beyond 'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models
- Declaring a friendship to self
- Internet Artifacts
    - discovered Helicopter game

#formal #forth #os #tla #zig
- Introducing oniux: Kernel-level Tor isolation for any Linux app
    - code
    - found smoltcp
- The cryptography behind passkeys
- How fast is CeTZ-Plot?
- ZJIT has been merged into Ruby
    - Instead of compiling YARV bytecode directly to the low-level IR (LIR), it uses an high-level SSA-based intermediate representation (HIR)
        - In the bytecode, which is tersely encoded, jumps are offsets, some control-flow is implicit, and most dataflow is via the stack.
        - By contrast, HIR looks more like a graph. Jumps have pointers to their targets and there’s no stack: instructions that use data have pointers directly to the instructions that create the data.
- found Warteschlangensimulator, a event-driven, stochastic simulator for queueing systems
- found kowk, a ~100k-pod k8s cluster simulator
- Data is code, about philosophy behind Forth
    - also What the hell is Forth?
- found Insights into DeepSeek-V3: Scaling Challenges and Reflections on Hardware for AI Architectures
- found Marigold: Affordable Adaptation of Diffusion-Based Image Generators for Image Analysis
    - Marigold Computer Vision
- Zig App Release and Updates via Github ⚡

#agent #ebpf #os #physics #rust #software #tui #web #yaml
- try genspark
    - impressive result
    - one deep research per day for free
- Read the Code, Not the Profile
    - Dramatic percentages in software is just linear improvement
- Writing that changed how I think about PL
- Experiment on your code freely with Git worktree
- Lock-Free Rust: How to Build a Rollercoaster While It’s on Fire
- found
    - Spall: a code profiler that runs in your browser
    - TUI for search & replace
        - scooter: Interactive find and replace in the terminal
        - serpl: A simple terminal UI for search and replace, ala VS Code.
        - scooter wins as it supports filtering files, both support regex and replace preview
    - Avian Physics 0.3
    - Makepad 1.0 : Rust UI Framework
- checked out YS — YAML Done Wisely
    - I wish to use it as a template engine, but the scripting syntax is not delicious
- Two months in Servo: CSS nesting, Shadow DOM, Clipboard API, and more
    - Servo is still very actively growing
- Misadventures in DTrace: how to debug the macOS kernel
    - I need to compare more with eBPF and DTrace
    - found DTrace book

#apl #formal #os #proof #rust #sec #tla #web
- Are We Serious About Using TLA+ For Statistical Properties?
    - found FizzBee for behavior correctness verification and performance modelling, based on simulation
    - I've wished for a tool like this for a long time
    - see also Modular verification of MongoDB Transactions using TLA+
- Flattening Rust's Learning Curve
    - The best open source project for someone might not be yours, and that's OK
- A review of documentation in the Rust ecosystem
    - found Blessed.rs: Recommended Crate Directory
- Secure by Design: Google’s Perspective on Memory Safety (2024)
- Microservices Are a Tax Your Startup Probably Can’t Afford
- Private Internet (2024)
- A tool to verify estimates, II: a flexible proof assistant

#os #rust #zig
- Memory Safety Features in Zig
    - very well summarized, with great examples
- Reservoir Sampling
- You can use C-Reduce for any language
- Rust Dependencies scare Me
    - a comment reminds me of Build It Yourself
- What's in an e-graph?
- A catalog of ways to generate SSA

#agent #gpu #idea #interop #os #software #web #zig
- Why transformers need adam: A hessian perspective[zhang2024transformers]
    - insightful, and well summarized related work
- trying to figure out a way to let AI agent to read all papers citing an paper, and write a summary of the follow-up research
- The magic of software; or, what makes a good engineer also makes a good engineering organization
    -  "Engineers are most capable and most effective when abstraction layers serve as shorthand for an understanding of what it is doing on your behalf, rather than a black box"
    - "start with deep understanding as the basis for innovation – cultivating the curiosity to look inside the black boxes"
    -  "The magic of both software and software organizations comes from those moments where insight into how something works sparks entirely new ideas about what it could become"
    - related: Reinvent the Wheel
- Implement your language twice
    - Futhark is a statically typed, data-parallel, and purely functional array language with AoT compilation to CUDA, OpenCL, HIP, and WebGPU (WIP)
    - also Comparing the performance of OpenCL, CUDA, and HIP
- Objective-C interop with Zig?
- got zig to work inside lima with minimal setup

#ebpf #os #rust #tui #zig
- Zig’s Low-Level Safety Features Leave Rust in the Dust
- found Parallel, Concurrent and Distributed Programming in Scala
- found nnd: A TUI alternative to gdb
- found A part of the fundamental group of an n-dimensional beanA
- Building a regex engine in C++
- wondering about chaos engineering in Zig with eBPF #ebpf
    - learn more about zbpf
    - maybe it's easiest to use lima to test eBPF
    - found Pixie when reading Debugging Production: eBPF Chaos
    - Introducing Minderbinder which is in Go
    - Implementing fast TCP fingerprinting with eBPF
        - using Cilium in Go
    - ebpf series - Unnamed Memories
    - Introducing TCP-in-UDP solution (eBPF)
    - Go Allocation Probe (on HN)
    - KernelScript eBPF-centric programming language (on HN) #lang
    - OOMProf - Take a heap profile just before OOMkill using eBPF #chaos
- found alternative open source front-ends for popular internet platforms
- Zig defer Patterns
- Glossary Web Component
- Recreating an iOS Animation with GLSL (interactive tutorial)
- found Argo CD - Declarative Continuous Delivery for k8s
- found bash/POSIX-compatible shell implemented in Rust

#agent #benchmark #blogging #context #formal #game #gpu #news #optimization #os
- LM
    - survey papers
        - A Survey on Inference Engines for Large Language Models: Perspectives on Optimization and Efficiency
        - Low-Precision Training of Large Language Models: Methods, Challenges, and Opportunities
            - sadly, NormalFloat used by QLoRA is excluded from the paper, as it is "specifically designed for pretrained fixed parameters, which only participate in the forward inference stage during training."
    - improvements on reasoning
        - Think on your Feet: Adaptive Thinking via Reinforcement Learning for Social Agents
            - the model is trained to switch between different complexity level of thinking mode based on context for an optimal balance between correct answer and reasoning length
            - the thinking modes are inspired by Hierarchical Cognitive Control Theory (HCCT)
        - RM-R1: Reward Modeling as Reasoning
            - provides good insight into reward modeling and how each training stage boosts the model's performance
    - other
        - Unlearning Sensitive Information in Multimodal LLMs: Benchmark and Attack-Defense Evaluation
            - I'm still interested in unlearning and model editing
- Benchmarking Crimes Meet Formal Verification
    - learn about Systems Benchmarking Crimes
- #zig
    - Implementing a Struct of Arrays
        - Zig has easy-to-use support of SoA via MultiArrayList
        - learn about Data-Oriented Design
        - I can't help but feel that new features of C++ such as reflection is really becoming syntax cancer
    - Reflecting on a year of Gamedev in Zig
    - Jai, the game programming contender
- bringing data to AI, not the other way around
    - The Data Surrender Trap: How Enterprises Are Losing Control in the AI Gold Rush—and the Simple Fix
- lifestyle
    - Protect The Habit
    - skimmed blogging in isolation
- skimmed modern-latex: A short guide to LaTeX that avoids legacy cruft
- The Beauty Of Having A Pi-hole
    - own your own DNS
- An appeal to Apple from Anukari regarding GPU frequency scaling
    - I'm amazed that the author is using GPU to simulate physics for realtime audio

#git #interop #lean #os
- found pyonji, a tool to support sr.ht style e-mail patches
- Git: programmatic staging
    - and learn about `grepdiff`, unfortunately, it's not available on Mac
    - `git add -p` is also acceptable for a small number of hunks
- MathML with Pandoc
- Starting on seamless C++ interop in jank
- found Anemll: Artificial Neural Engine Machine Learning Library

#formal #os #web
- DeepSeek-prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition[ren2025deepseekproverv2]
    - A survey on post-training of large language models[tie2025survey]
        - notes on LM could be based on this survey and the following papers related to r1
    - 100 days after DeepSeek-R1: A survey on replication studies and more directions for reasoning language models[zhang2025days]
        - Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning[guo2025deepseek]
            - should revisit
    - found critics of r1/GRPO
        - Understanding r1-zero-like training: A critical perspective[liu2025understanding]
        - Does reinforcement learning really incentivize reasoning capacity in LLMs beyond the base model?[yue2025does]
    - Kimina-prover preview: Towards large formal reasoning models with reinforcement learning[wang2025kimina]
- found A Survey of Interactive Generative Video
- Polishing your typography with line height units
- Solving Sudoku with Algebraic Geometry and Computer Algebra : A C Programming Approach

#apl #formal #lean #os #prolog
- found Leanabell-prover: Posttraining scaling in formal reasoning[zhang2025leanabell]
- skimmed Flow matching guide and code[lipman2024flow]
- APL: Comparison with Traditional Mathematics
- I use Zip Bombs to Protect my Server
- found Prolog Notes
- found Quotes on notation design & how it affects thought

#agent #os #✍️
- found A Dependently Typed Assembly Language
- Qwen3: Think Deeper, Act Faster
- found Topologies and Sheaves Appeared as Syntax and Semantics of Natural Language (2012)
    - reveals connection between sheaf theory and linguistics
- found On the expressivity role of LayerNorm in transformers’ attention[brody2023expressivity] [code]
- found Grammar prompting for domain-specific language generation with large language models[wang2023grammar]
- wrote My setup with 4 screens and 2 Macs

#compiler #llvm #os #zig
- BitNet v2: Native 4-bit Activations with Hadamard Transformation for 1-bit LLMs
- Converting a C API to Zig with the help of comptime
- How a Single Line Of Code Could Brick Your iPhone
- found Nouveau: The Rule Based Language Family
    - and easily got into an infinite loop by adding a rule trying to combine a match and a box back to a matchbox
- Technical Debt as Theory Building and Practice
- Using HAProxy to protect me from scrapers
- What if we embraced simulation-driven development?
    - Notes about ETCD, there are some war stories
    - Notes about Raft's paper
- toycalculator, an MLIR/LLVM compiler experiment.