ashton314

Regretting my choice to do a PhD in CS instead of whatever this cool thing is…

Kent Dybvig also wrote Chez Scheme [1] which on most benchmarks is far-and-away the fastest [2] Scheme implementation.

Racket recently got rewritten to be based off of Chez [3] and I have it from the maintainer of Racket himself that it’s paid off well: better performance and a smaller, more maintainable codebase.

1: https://github.com/cisco/ChezScheme (also, pronounced “Shay Scheme”)

2: https://ecraven.github.io/r7rs-benchmarks/

3: https://m.youtube.com/watch?v=s3Q3M2wZ7rI&pp=0gcJCRsBo7VqN5t...

> breaking changes

Yeah, that's bitten me and it's super stupid. At this point, I've just pinned hugo so I don't update it any more. It's a friggin' static site with basically no Javascript (just a little for the site search feature—handled by the theme) so I don't feel any need to keep Hugo up-to-date.

You would certainly enjoy using it then. :) It's got great documentation. (As is to be expected with basically any Emacs project.)

Equations: very yes. You have to create some custom short codes. Example of it in action here: https://lambdaland.org/posts/2024-08-06_zkp/

Here's the source for that entire post: https://gist.github.com/ashton314/e63c9ed31c38c421f11d84df1f...

The shortcodes are a little messy, I will admit, but I have a temp.el snippet that expands to the right thing so authoring isn't too bad.

org-babel: I'm not sure. Here's the docs for code block handling in ox-hugo: https://ox-hugo.scripter.co/doc/source-blocks/

^ This. Hugo's support for Markdown is much better than it's support for org-mode. ox-hugo bridges the gap super well.

This is a nice feature of ox-hugo. I still use individual files and it's great.

I used Hugo's native `.org` file support for a while. It was… fine. There are some serious issues (for me) that I had with it though. The most salient one is that it didn't convert straight quotes in the source ("") to proper curly-quotes. (“”) I don't remember what else but I'm sure there was more than just that. I've spent a lot of time on the typography of my site and I wanted everything to be as perfect as I could make it.

I write my blog (https://lambdaland.org) entirely in Emacs now. It's Hugo, but I use ox-hugo [1] to convert from org-mode to markdown and Hugo converts it to HTML.

What I like about this: everything else I do is in org-mode anyway, so this fits my brain. I also have some nice org-mode tooling to make things like footnotes, margin notes, etc. look really nice.

A little convoluted, sure, but I've seen worse. :-P

[1]: https://ox-hugo.scripter.co/

So, what's the best way to fight back, personally and collectively? Yes, yes—we need legal measures against this sort of thing—but are there tracking mitigation measures that known to be effective on mobile devices? Is there a way we can dilute this commercially-available data to poison the well, as it were?

Not quite: Codeberg discourages you from having too many closed source projects, but you can absolutely have private repositories. I have several.

They explain the rules here: https://docs.codeberg.org/getting-started/faq/#how-about-pri...

This is called “the dead horse paper” for some reason. There’s been some interesting work since. This isn’t my exact area of research, but I’m pretty well versed in it and I work with one of the authors on this paper so I’m happy to try and answer any questions.

The chief issue here is how do you assign blame to typing violations? Typescript is unsound: since it just erases types, an untyped library that a typed component is using might return something the typed component isn’t expecting leading you to get a type error in typed code. Gradually typed python variants typically are better, though they usually just inspect the shape of the data and don’t check that eg every element in a list is correctly typed as well. This can lead to more unsound behavior. Typed Racket is fully sound, but performance can degrade spectacularly.

There’s been some work reviving the dead horse being beaten in this paper. Lmk if you have questions.

More papers:

Muehlboeck, Fabian, and Ross Tate. “Sound Gradual Typing Is Nominally Alive and Well.” Proceedings of the ACM on Programming Languages 1, no. OOPSLA (October 12, 2017): 56:1-56:30. https://doi.org/10.1145/3133880.

Moy, Cameron, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. “Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification.” Proceedings of the ACM on Programming Languages 5, no. POPL (January 4, 2021): 53:1-53:28. https://doi.org/10.1145/3434334.

Lazarek, Lukas, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. “How to Evaluate Blame for Gradual Types.” Proceedings of the ACM on Programming Languages 5, no. ICFP (August 18, 2021): 68:1-68:29. https://doi.org/10.1145/3473573.

Fellow PL grad student—not a top-3 tho ;)

I’ve looked at Typst and it looks attractive. I’m not quite willing to invest in it until, say, PACMPL lets me use it there. Any idea if that will happen any time soon?

Well, they put a sign on the trash can that says “this is in fact on fire” so you know that they’re aware it’s a dumpster fire.

Sam will definitely know more about this than I will, so if he contradicts me, listen to him.

If I am not mistaken, the racket language does not convert to CPS during compilation. Instead, when you want to get the continuation, I think you just get a pointer to the stack frame that you want. All I know for sure is that it uses something called a-normal form, which is kind of like SSA in some ways, and that the continuation is 2x 64/32-bit words depending on your architecture.

Some amount of this has got to be due to Covid. I used to tutor a middle school boy, and he was probably two years behind where he should have been. Because of this, he was lacking the foundation that he needed to progress. It was so bad.

Undefined behavior does not violate correctness. Undefined behavior is just wiggle room for compiler engineers to not have to worry so much about certain edge cases.

"Correctness" must always be considered with respect to something else. If we take e.g. the C specification, then yes, there are plenty of compilers that are in almost all ways people will encounter correct according to that spec, UB and all. Yes, there are bugs but they are bugs and they can be fixed. The LLVM project has a very neat tool called Alive2 [1] that can verify optimization passes for correctness.

I think there's a very big gap between the kind of reliability we can expect from a deterministic, verified compiler and the approximating behavior of a probabilistic LLM.

[1]: https://github.com/AliveToolkit/alive2

Compilers use heuristics which may result in dramatically different results between compiler passes. Different timing effects during compilation may constrain certain optimization passes (e.g. "run algorithm x over the nodes and optimize for y seconds") but in the end the result should still not modify defined observable behavior, modulo runtime. I consider that to be dramatically different than the probabilistic behavior we get from an LLM.

Looks like there's a year at the end; might be to facilitate suckurity requirements such as yearly password rotation.

Oo I’m excited for this. The old official language server is fine—it does its job on most of the code bases I’ve worked on, but occasionally I will do something funny that makes the compiler slow down and that pummels the LS performance. I hope this works out some of the kinks that occasionally would make elixir-ls slow.

Fair, fair—it's default is longer, so dialing it down made it feel zippy by comparison.

I'm trying out Homerow and I'm really liking it! Thanks for mentioning it. I might end up sticking with it actually.

As I understand it, a payment system is in the works. I would gladly fork over some cash to support ShortCat. Looks like someone recommended Homerow, which appears to be pretty comparable to ShortCat, and it has a one-time purchase option.

This delay is configurable. The delay is there so you can actually type a bit before the UI pops up, and then the UI will be filtered to just your selection.

For macOS users, I highly recommend ShortCat: https://shortcat.app/

ShortCat uses the accessibility API to put Vimium-style keyboard links on buttons and text fields in any app.

I find that Vimium works faster in Firefox than using ShortCat to click around websites, so I use both, but ShortCat technically should do everything (clicking-wise) that Vimium does.

> So, go is a perfect fit for the http server (or service) usecase and in my experience there is no parallel.

Elixir handling 2 million websocket connections on a single machine back in 2015 would like to have a word.[1] This is largely thanks to the Erlang runtime it sits atop.

Having written some tricky Go (I implemented Raft for a class) and a lot of Elixir (professional development), it is my experience that Go's concurrency model works for a few cases but largely sucks in others and is way easier to write footguns in Go than it ought to be.

[1]: https://phoenixframework.org/blog/the-road-to-2-million-webs...

Very cool!

I did something like this with pandoc:

    pandoc -s -t man "$1" | groff -T utf8 -man | ${PAGER:-less}

Keeps a lot or formatting. My favorite way to read a README file in the terminal

Lemme guess: you might think that everyone should just write their blogs on Substack, right?

The web thrives on diversity. More forges is good.

Furthermore, GitHub has been making moves that understandably worry some and so it’s great that there are some excellent alternatives.

I don't get that emotional when watching movies. I cried a little when the parachutes opened in Apollo 13.

As a kid I had a book detailing hundreds of space missions—mostly probes, obviously—but my favorite mission to read about was Apollo 13. Just incredible.

Maybe when Jim got to heaven, the first place the angels took him to was where he would have landed on the moon.

Computers can do a lot of human jobs. But something I believe is fundamental to the human experience is the connection with other humans. Using an LLM or similar technology as a means to circumvent or shirk such connection is reprehensible. Using a computer to do another job is fine.

It’s incredibly trust-eroding.