Aaron Moss @bruceiv@types.pl

Okay, so private-equity ghouls are literally reviving coal plants to mine Bitcoin...

https://arstechnica.com/tech-policy/2021/05/private-equity-firm-revives-zombie-fossil-fuel-power-plant-to-mine-bitcoin/#p3

Can someone on types.pl tell me what the big advantage for variant types over union types is?

In particular, I've been trying to teach Rust error handling, and it seems like it would be easier if I could say "this function returns either an error or a f32" rather than "you need to wrap the output like Ok(3.14), or if there's an error it looks like Err(OurErrorType("bad"))"

On the topic of big ships and sea shanties, Roll Northumbria by the Dreadnoughts has been stuck in my head all week: https://youtu.be/-d3XHQVMHDM

What is the Ever Given but a sandbar persevering?

Anyway, I was musing on this in some idle time this morning, but formal methods is really not my end of PL (I'm more on the compiler-construction end), and I figured someone here might know more on the topic.

I'm more interested in an "assertion failure" level of checking than "mathematical proof of termination", but if you just had an analysis on (unsigned) integer ranges, and some sort of "bounded" attribute tag for your collection types that are actually bounded, would a compiler be able to statically determine that most(?) common recursion and looping patterns would actually terminate? Would the level of extra annotation required be acceptably small (i.e. you could teach it to a beginning programmer in under an hour)?

I think the only(?) places where you get divergence are unbounded (or improperly-bounded) loops or recursion (and maybe panics/assertion failures, which we analyze the same-ish way).

I'm thinking of something like adding `noreturn` as an expression type, possibly unioned with other types.

What are the barriers to building a type system that encapsulates knowledge about program termination?

TIL Swift has ports to Linux & Windows (hopefully they work well for my PL students who've chosen Swift for their final projects...) https://swift.org/platform-support/

Password reset at work this week, which means my login password has been <old password> -- "invalid" -- <new password> for days

The best "goof" note for Home Alone:

Well, at least I got one thing done in 2020 - I spent at least a bit of time learning German (almost) every day.

Been watching Farscape, and getting convinced that Gritty is actually a Luxan.

With all the calls for "healing" and "bipartisanship", I've been thinking of the treaty negotiation scene in this season of Star Trek: Discovery. Admiral Vance would love to see a productive alliance between Starfleet and the Emerald Chain, but won't bend on Osyraa facing a fair trial and appropriate consequences for her crimes, because you just can't work with someone who's willing to see you dead if they don't get their way. Dr. Aurellio learns a few episodes later what happens if you're willing to work with a murderer - eventually, they either make you join in their murder, or they kill you.

Biden, Schumer, and Pelosi could learn some lessons. I think there's value in bipartisanship, compromise, and reaching across the aisle, but your interlocutors need to have some common values and a willingness to work within the system in good faith. Half the GOP House caucus and six Senators voted against the democratic will of the American people, many of them after inciting the mob that tried to overthrow that democracy by force. There need to be conditions on the open hand of bipartisanship, and a clear one is that Republicans need to make a clear stand against mob violence, and expel the seditionists like Trump, Cruz, and Hawley from their party, and in at least Trump's case, from his office as well.

I'm not optimistic, but I've read about the failure of Reconstruction after the Civil War, as well as the Beer Hall Putsch a decade before the Nazis took over Germany, and if the USA wants to still be a democracy in a decade's time, there needs to be a clear stand for democracy now.

Useful advice for anyone applying for grad school/PhD program (at least in CS): http://composition.al/blog/2020/11/25/how-not-to-email-prospective-grad-school-advisors/#fnref:1

And the coding question worth 20% of the midterm was ambiguously worded ... just a whiff all around.

Not my finest teaching day today ... after the midterm was done I realized I'd accidentally taught them Dijkstra's algorithm and called it Prim's, and not taught them the definition of complete binary tree before I put it on the test.

This etymology of the word "ampersand" is delightful.
https://en.m.wiktionary.org/wiki/ampersand#:~:text=Etymology,originally%20referred%20to%20in%20English.&text=This%20last%20phrase%20eventually%20became,English%20usage%20by%20around%201837.

Gotta say, watching the local Oregon/Portland votes come in is soothing. They're mostly not going the way I'd like, but choices between liberal and progressive don't fill me with the same existential dread