bmc7505

* Not to be confused with the homonymous Sky News [1].

[1]: https://en.wikipedia.org/wiki/Sky_News

jart may see her wish come true after all

  "Life imitates art far more than art imitates life."

—Oscar Wilde, The Decay of Lying (1889)

Tridactyl is awesome! There are also many similar plugins for different web browsers and text editors: https://github.com/acejump/AceJump#comparison

There are architectures with layers which can approximate MAXSAT [1] (or rather, an SDP relaxation thereof), but I doubt this is what OP was referring to.

[1]: https://arxiv.org/abs/1905.12149

“The Sapir–Whorf hypothesis has been thoroughly debunked by fact-checkers at the Ministry of Truth and determined to be fake news.”

Well, how reassuring!

  "Don't you see that the whole aim of Newspeak is to narrow the range of thought? In the end we shall make thought-crime literally impossible, because there will be no words in which to express it." 

—George Orwell, 1984 (1949)

There is an interesting algorithm for sorting that is highly amenable to parallelization and which I thought this article was going to be about: https://en.wikipedia.org/wiki/Sorting_network

Well said. You think clearly. Who are you?

There is a statue commemorating the fallen soldiers of the Boer War in Auckland: https://goo.gl/maps/Wh8BfAnFFVU7ZbQFA

SPLASH had another keynote on pattern languages this year. The analogy from architecture to programming languages seemed strained at best - the speaker spent most of the talk on social programming, i.e., programming humans how to act in certain social situations and making design concepts more explicit and user-friendly. He made a big fuss about what a successful consultancy he built around running workshops and distributing baseball cards with different patterns printed on them. I found the whole thing self-aggrandizing and borderline charlatanry for an academic PL conference.

I stayed at the Radisson in 2019 for ICFP and was astounded at the poor quality of the building, which was undergoing renovations at the time. I distinctly remember noticing visible corrosion around the foundation of the tank structure.

As a frequent Amtrak passenger, I can attest to the unpunctuality of the Union Pacific and other freight operators. On several occasions we have been delayed by a passing freight train that was an hour or more behind schedule, causing us to miss our scheduled connection. During one such occasion, while traveling on the Coast Starlight from Eugene this summer, I was treated very rudely by the conductor, who kicked me out of the dining car despite having a reservation. Precision scheduled railroading is anything but precise.

I had always heard this saying as an undergrad in CS but never understood why names were supposed to be a hard problem until reading about modal logic about a decade later.

https://en.wikipedia.org/wiki/Naming_and_Necessity

Also: https://www.thestrangeloop.com/

Related: https://news.ycombinator.com/item?id=33585154

Related: https://news.ycombinator.com/item?id=32780397

Uncanny.

Interesting bit of trivia, Prof. Ratzer, the author of this piece, was the first graduate student in computing at McGill University [1] and one of the founding members of the School of Computer Science [2], which just recently celebrated its 50th anniversary. [3]

[1]: https://en.wikipedia.org/wiki/McGill_University_School_of_Co...

[2]: https://www.cs.mcgill.ca/~ratzer/backup/welcome.html

[3]: https://mcgill.imodules.com/controls/email_marketing/view_in...

The way I read this is that computers are a bit like telescopes, in that they allow us to appreciate the structure of the [logical] universe. These instruments sharpen our limited powers of observation, allowing us to see farther or more clearly than we would otherwise be able to do with merely pen and paper.

“Computer Science is no more about computers than astronomy is about telescopes.” — E. W. Dijkstra

In theory, yes, but in practice proof assistants are only just starting to become practically useful for research-level mathematics. Validation/verification would likely require an enormous amount of proof engineering to build up the theorems required to verify a proof of this complexity. See the Liquid Tensor Experiment postmortem [1] for the results of a similar undertaking.

[1]: https://leanprover-community.github.io/blog/posts/lte-final/

During a recent programming adventure, I discovered that finite elementary cellular automata with periodic boundary conditions can be simulated using matrix-vector multiplication with a circulant matrix and a strange kind of algebra, which I call a kernel algebra. [1] I wonder if this same idea could be generalized to higher dimensional automata on other topological surfaces.

[1]: https://github.com/breandan/galoisenne/blob/8f0f1e9e4e02062c...

  > Well, your own link proves it, doesn't it?

That code simulates a bounded cellular automaton, which effectively reduces to a regular language, but that's about as far as I've been able to get. If it's possible to implement general recursion, I'm not quite sure how - yet.

  > Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable.

They're not using Kennedy and Pierce's system, but it's closely related. See Tate (2013) [1], in particular, "In general, since declaration-site variance can easily be encoded into use-site variance..."

  > I ported that code directly to Kotlin

Can you share your translation of Eric's code? Maybe we can get it to work.

[1]: https://fool2013.cs.brown.edu/tate.pdf

  > One person noodling around for a few weeks

Well, I've been trying for about three years, but to be fair I'm a pretty slow programmer so you may have better luck.

  > a language being too obscure to have seen much academic study

Doesn't seem too obscure to me. https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=kotl...

  > T isn't generic in that code, it's just a class.

I think it needs to be a generic type in Kotlin for this to work, because otherwise it will dispatch to a single method. It's tricky to get Kotlin to do much compile time computation. Not saying that it's impossible, but LMK when you've actually tried it. Here's some sample code if you want to try encoding a Boolean logic:

https://github.com/breandan/galoisenne/blob/2e465e7a753f6341...

Try it! I certainly have. You may find encoding a typelevel TM or λ-calculus more difficult than it appears...

  > link's example for C# would translate directly into Kotlin

T() is not possible for a generic T in Kotlin.