I've been burned by this a few times and now I have the Hugo binary in source control. I had to dig through the releases a little bit to find the version that didn't break everything.
Woohoo! Context: UNIX v4 was believed lost to history until a tape labeled “UNIX v4” was found in a cardboard box in a closet at the University of Utah. It was not clear whether or not there was anything on the tape still. It looks like the Voeks at the Computer History Museum were successfully able to recover the data.
This is significant because UNIX V4 was the first version to be written using this newfangled language called C. So exciting!
What do you do now? I’ve been buying physical books off of Abe Books—not a bad thing at all—but I’d like to use my jailbroken kindle again because the form factor is so convenient.
Buy DRM free when you can. Not only is this convenient for you but will hopefully help nudge the market. When you can't, buy the book from one of the easily cracked sources (Kobo, Google, Adobe DRM).
Or you can save yourself the bother of removing DRM by buying the book from wherever and then downloading a copy from Anna's.
I try to buy physical books, and make an effort to buy it elsewhere, with AMZN being the reluctant last resort if I truly can’t find it. I don’t have a specific go to place anymore.
Also, I reduced the buying pace - owning physical books takes up space, so the bar for getting something into the library is now much higher than before.
It’s a shift but I agree. I think we’re used to having instant access to what we want. Waiting 3 weeks on Libby is a change. I do think it’s been healthy and gives me something to look forward to!
> … verify/synthesize invariants in languages people use?
Good question. This is the holy grail. This is what everyone in PL research would love. This is where we want to get to.
Turns out a language as “simple” as C has sufficiently complicated semantics as to limit rigorous analysis to the basics. One example is loop analysis: it’s very useful to know that a loop will terminate eventually; if a loop is modifying some state and—worse—if the iteration variable gets modified—kiss your analysis goodbye because mechanically synthesizing strong pre- and post-conditions becomes insurmountable. It’s not an engineering challenge. It’s a math/pure CS theory challenge.
Right. The problem is that those languages are relatively permissive in their type systems. Obviously Rust can capture more in its type system than C can. You would probably want a type like “decreasing unsigned integer” for Rust and some way to enforce monotonic decreasing, which Rust doesn’t give you.
(Any experts on formal verification please correct any inaccuracies in what I say here.)
The upshot of it is that C, C++, and Rust permit too much behavior that isn’t capturable in the type system. Thus, the properties that you’re interested in are semantic (as opposed to syntactic; type systems turn semantic properties into syntactic ones) so Rice’s theorem applies and there’s no computable way to do the analysis right.
This is written by Matthew Butterick—a lawyer, typographer, and programmer. He's got another online book called Practical Typography that will help you appreciate (and make!) good typography: https://practicaltypography.com/
The site is really fun: at the bottom you can change the body text from Valkyrie to Equity, Concourse, etc. (these are all fonts that he made).
His books are made with a Racket-based publishing system called Pollen. I've used it a little bit and it's nice: it's incredibly flexible, so you have to do a lot of work to get what you want out of it, but it also doesn't confine you.
He's made some gorgeous typefaces: https://mbtype.com/ His license is far and away the most permissive non-OFL license I've encountered: buy the font once for the lowest price I've seen in a professional font, and then you can use it pretty much everywhere indefinitely. So nice.
I use two of his typefaces (Valkyrie, similar to Palatino, and Hermes Maia, a sans-serif based off of a German typeface) on my blog so you can see it in action: https://lambdaland.org/
I hear you: I don't like how skinny the letterforms are. There's an "extended" variant that I find much more pleasing. I put together a customization you can see here: https://codeberg.org/ashton314/iosevka-output (there's a nice screenshot on that page).
You can probably get the proportions you want if you find a way to tweak the line spacing (also possible by adjusting the `leading` option in `private-build-plans.toml` and rebuilding).
reply