Oglaf comic of scented candles, bzowts, and misogyny. #humor #NSFW
SBC-XQ is a #Bluetooth hack to get better sound quality out of the SBC codec mandated by A2DP (Advanced Audio Distribution Profile, which I think is “high fidelity playback”) #audio
more discussion of #Bluetooth SBC-XQ #audio
#PDF of Butler Lampson’s 01983 #paper “Hints for Computer System Design” which describes how to “Use Hints” in the Xerox PARC Alto filesystem
Originally the “different strokes for different folks” were different ways Muhammad Ali punched out different boxers. #history #humor
The #Lean homepage uses “L∃∀N” as the logo but says, “Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code”. #formal-methods
#Lean online playground storing the code in an URL fragment. This is supposed to be a solver for a couple of linear inequalities. But it takes forever to load and then I can’t figure out how to actually run anything.
#video on the "ElectroHelix" #TENS #neurostimulation #electronics #hardware for play parties from e-stim.co.uk. It uses 2mm pin connectors on the ends for medical sticky-pad electrodes. Their knobs (“level”, “feel”, “speed”) are not calibrated at all. 84000 views! #sex
#video on Anisha Patel’s #TENS #neurostimulation #electronics #hardware for muscle stimulation. No explanation.
#Tutorial #documentation directory for #Lean 4, starting with the Natural Number Game. #toread
The Natural Number Game #tutorial for #Lean 4, starting with rfl and rw [assumptionname]. #toread
#PG wrote about how to become a billionaire, saying he’s trained about 30 billionaires to do so successfully. He’s right about the virtues of capitalism, but he’s glossing over #enshittification.
#Switzerland rejects the 10-million population cap referendum! 55% voted no, 45% voted yes, with 59% turnout (48% being average turnout.) #news
Yaron Minsky at #Jane-Street, the guy Will has been talking to, wants to adopt #formal-methods now, though previously they haven’t because of the costs. “And those costs are really high! seL4 is a great example of this. It’s a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.” But now they have “agentic coding”, meaning #AI.
discussion of #formal-methods in the context of #Jane-Street, including #John-Nagle. #toread
#ebook of the Pascal-F verifier from 01985 by Scott D. Johnson and #John-Nagle. #formal-methods
new #Primitive-Technology video, building a new hut with previously fired clay bricks and mud mortar with a little bit of wood ash added to grout it. He makes a plumb bob and shows why he should have had it before. Also he shows an unsuccessful #firestarting attempt before the successful one, saying that this is common in humid weather.
