GitHub: https://github.com/ashton314
Blog: https://lambdaland.org
- ashton314 parentIf you just wait a few months, then that program will be written in a typed language. The type checker for Elixir is coming along nicely and every release brings more checks.
- 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!
- 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.
- > … 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.
- 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).
- Here’s how you can clear it:
https://github.com/orgs/community/discussions/174310#discuss...
I had the same issue too, and this was the only thing that fixed it for me.
- A analogy: For the same reason why natural wood is more beautiful than plastic. Natural wood gets its beauty from little faults and irregularities. The process of growing a tree takes a long time and thereby is more valuable. A plastic facsimile can be made to look similar and be cheaper to produce, but it lacks the unique grain and quality of the wood.
It’s not just the end product that matters. The process and intent behind its genesis matters too.
- These are small benchmarks, so don’t over-generalize from this data point alone, but Racket absolutely crushes Python in terms of speed and goes speedily enough against other popular performance-focused languages:
https://lambdaland.org/posts/2023-12-20_functional_langauge_...
https://lambdaland.org/posts/2024-09-27_threaded_interpreter...
Matthew Flatt, the Racket lead, says that Racket’s performance should be fairly comparable to Java, much faster than Python, slower than Julia/Rust/etc. That’s been a helpful model for me: if Java is fast enough, Racket will do fine.
- I watched Typst from afar for many years. I finally took it out for a spin about a month ago after version 0.14 dropped.
In less than an hour I reproduced my résumé—complete with fancy functions to typeset employment entries on a grid system. In under 24 hours I was tinkering with the Typst source code.
Typst is amazing. Syntax is clean and consistent. The compiler is so so fast. Docs are excellent. And it is very close to TeX when it comes to typesetting quality. There are a few tiny rough edges that any \usepackage{microtype} enjoyer will miss, but stuff is improving rapidly.
(Also, XKCD disclaimer: this was not an LLM—I just use em-dashes a lot because TeX made them easy to type and I got used to having them.)
- Author here—happy to answer any questions.
The website I link to is really quite fascinating if you haven't seen it already: https://arewedecentralizedyet.online/
Go decentralization!
- Typst is so stupidly easy to use. It took me an hour to go from zero Typst knowledge to reproducing my résumé perfectly. The docs are easy to read and there’s a guide for making templates. I feel like if you’ve written CSS and are familiar with associating some kind of selector with some properties, then you’ll be able to pick up Typst and make whatever template you want in no time.
- Racket really shines in this regard: Racket makes it easy to build little DSLs, but they all play perfectly together because the underlying data model is the same. Example from the Racket home page: https://racket-lang.org/#any-syntax
You can have a module written in the `#racket` language (i.e., regular Racket) and then a separate module written in `#datalog` and the two can talk to each other!
- I maintain a pretty popular Emacs starter-kit called Bedrock. [1] I suggest starting with it, or at least taking a look at it to get some ideas!
Bedrock differs philosophically from Doom et al. in that Bedrock is meant to be as simple as possible. There's no magic, no extra package management system (looking at you Doom) to break or confuse. By default, it doesn't install any 3rd-party packages—it just sets better defaults. Recent versions of Emacs can do a lot, but the defaults are painfully outdated. Bedrock fixes that. It's basically a vanilla Emacs experience without some of the cruft carried over from the previous century.
Bedrock also comes with a curated set of packages to enhance Emacs beyond better defaults. You can load these into your config as you begin to need them. List here: [2] If you are looking for a set of "modern" packages, this is it. I do pretty well keeping up in this space, and a lot of these (esp. Vertico, Consult, Corfu, etc.) seem to be accepted as the de-facto best replacements for older packages like Helm, Ivy, etc. (That said, I should add some config for Casual—very neat package to help with seldom-used features of Emacs.)
Bedrock is meant to be understandable: clone it once, and then tweak from there. You'll find a lot of forks of Bedrock on GitHub as people have forked it and then built their own config on top.
I'm working on updating Bedrock for Emacs 31. There won't really be that many changes, so like, don't wait for 31 to start your Emacs journey, but know that Bedrock is actively maintained and that the packages I've curated for it are the best I could possibly find. :)
Oh, also, if you search "best Emacs packages", my blog post [3] will come up on the first page on basically every search engine I've tried. ;)
Happy hacking!
[1]: https://codeberg.org/ashton314/emacs-bedrock
[2]: https://codeberg.org/ashton314/emacs-bedrock#extras
[3]: https://lambdaland.org/posts/2024-05-30_top_emacs_packages/