a ton of crates

my most gamer trait is that i will put on some shit like Animal Crossing Lofi Hiphop Chill Music and instantly become 20% more relaxed and happy

separation logic renderers
🤝
anti-aliasing

when my food wrapper says ᴄᴏɴᴛᴀɪɴꜱ ʙɪᴏᴇɴɢɪɴᴇᴇʀᴇᴅ ɪɴɢʀᴇᴅɪᴇɴᴛꜱ i whisper back hell yeah, brother

for professional software dev we're starting to have some data though (which sourced my 25% estimate):
papers.ssrn.com/sol3/papers....
metr.org/blog/2025-07...

i would believe that AI could make you ~5x faster at ramping up with a tool (prog lang, low-code system, etc.) but not w/ expert use

what's stupid about "upskill w/ AI or die" is that we're currently talking about at best a ~25% productivity gain. that's probably in the same category as "learning all your IDE features", but govts / corps aren't in a full panic to push LSP onto everyone

not your question but TIL that you can sneak around the abstract cycle checker w/ GATs and defer cycle checking to concrete types play.rust-lang.org?version=stab...

i would probably focus on dependency updates, specifically tools for:
- checking for semver hazards (eg crates.io/crates/cargo...)
- automatically patching downstream codebases (eg ast-grep.github.io/advanced/too...)

it rocks to give your job talk in a non-judgmental setting

bsky.app/profile/tono...

*precisely* unknowable, but there's a lotta room for approximately knowable

conversely, a substantive portion of expertise w/ using program analysis is building an intuition for how to avoid these cliffs

possibly *the* foundational problem in program analysis is complexity cliffs: usability is not linear. once your program surpasses a threshold of complexity, everything goes to hell.
- type errors become useless
- program slicers miss dependencies
- SMT solver heuristics give way to O(2^n)
- etc

true, i am local-open-pilled and also wish ocaml adopted modular implicits

in ocaml wouldn't you use infix here? like

my_opt
>>| fun x ->
let y = computation_on x in
...

i don't quite follow why those mechanisms would make lean more suitable as a systems programming language

and after all, lean is not designed for computing :P

imo writing high perf / low footprint code has to be a first class concern in the language design, not punted to the compiler. i can imagine there will be restricted subsets a la Low-* with reliable code generation but whether that approach works at scale is very much unknown

hmm unclear what would replace it though, and a replacement would need an enormous amt of effort, luck, and momentum. the c++ behemoth has been going for 40yrs and probably won't be slain for at least another decade

very bullish

"the university's free tuition for underprivileged students is unlawful because it might, as a side effect, remedy racial inequality" is possibly the most evil argument ever advanced in american law. slavery was of course more evil, but defenses of slavery were bad-faith paternalism.

- match makes me feel like 4 years spent learning Standard ML was not wasted

although ftr i do prefer:
- match follows ltr reading order
- labeled None case is preferable is the Some case is large
- match permits one-liners w/o braces

we can put this debate to rest by calling for all programming languages to immediately adopt the Ultimate Conditional Syntax

no, it's just a silly way to write what is more directly & generally expressed as a match expression

every day someone writes `if let Some(x) = e1 { e2 } else { e3 }` we stray further from the light

iirc last time i encountered this was bc of coercions, which are hidden by default in the goal pane's pretty printing

this diagram is immensely funny to me because people like @shriram.bsky.social will tear their hair out over vague statements about strongly-typed languages. meanwhile systems researchers are just like "Type Systems Can Be Totally Ordered And I Will Plot Them'

screenshot of fig 1 from ousterhout's dichotomy paper. graph w/ x-axis is "degree of typing" and y-axis is "instructions/statement". bottom right is c, c++, and java labeled systems programming. top-left is tcl/perl, visual basic labeled scripting

ousterhout solved this problem three decades ago by bravely declaring java a systems programming language

not really... everything i've done i wrote from scratch just w/ components like codemirror. what kind of comprehension are you measuring?

yeah codeql is very much beneath my baseline for "good", at least in my limited experience with it for doing interprocedural stuff