Hi Jake! Cool article, and it's something I'll keep in mind when I start giving my self-hosted setup a remodel soon. That said, I have to agree with the parent comment and say that the LLM writing style dulled what would otherwise have been a lovely sysadmin detective work article and didn't make me want to explore your site further.
I'm glad you're up to writing more of your own posts, though! I'm right there with you that writing is difficult, and I've definitely got some posts on similar topics up on my site that are overly long and meandering and not quite good, but that's fine because eventually once I write enough they'll hopefully get better.
Hi! Yes, I talk about this a little bit at the end and I solve Part 2 the normal way. This is a toy example that I did for fun. The objective was to introduce people to Program Construction and show how you can use formal methods to derive correct programs. Whether the juice is worth the squeeze is a judgement call that you make depending on how critical the software you are writing is.
It's compiled to Erlang, not BEAM bytecode, as the latter is not a stable, backward-compatible API to target, and you lose all of the optimization work put into the Erlang compiler. It's also compiled to JavaScript, so it can run on both the front-end and back-end.
Not sure what the legal technicalities are, but one of the questions I saw on the site was just a picture of a the user's screen with the question on it, so it's definitely more the former than the latter.
I'm glad you're up to writing more of your own posts, though! I'm right there with you that writing is difficult, and I've definitely got some posts on similar topics up on my site that are overly long and meandering and not quite good, but that's fine because eventually once I write enough they'll hopefully get better.
Here's hoping I'll read more from you soon!