27 comments

[ 3.0 ms ] story [ 71.2 ms ] thread
I love the name of this paper. It's a play on Gödel, Escher, Bach: An Eternal Golden Braid by Douglas Hofstadter.

https://en.m.wikipedia.org/wiki/Gödel,_Escher,_Bach

(comment deleted)
Came here to see if I was just imagining things. Thanks for confirming!
Glad I wasn’t the only one who saw the reference! Now I just need a version that ties in M.C. Escher’s impossible staircases with infinite loops.
My mind was boggling over a JMW Turner connection to Hofstadter!? Guess I don't know CS ..
I was really excited to see how a 19th-century landscape painter was connected with one of the best NBA players of the 1980s and an Ancient Greek mathematician. Not what I got, but the actual subject is still pretty interesting.
[flagged]
(comment deleted)
Turner hoped that we could have programming languages that wouldn't go into (useless) infinite loops. They should either terminate, or keep producing values forever (be 'productive').

The author sets out to prove that Bird's version of the prime number generator (Sieve of Eratosthenes) is productive.

Fwiw I'm lost almost immediately in section 4 - the actual proof.

I think I get one point, which is to immediately ignore the actual values of the primes, and only prove that they keep being generated (which I guess is the purpose of `approx`), but I'm immediately lost by the overall strategy:

  that is, not so much showing that primes spec is a fixed point of makeP · makeC, but that it is the least fixed point.
My programming languages course in college had a section on Miranda. That’s 25 years ago and I’ve forgotten almost all of it, and I am not a Haskell programmer. But those few weeks proved essential for me and has benefitted my C++ tremendously.
I've written a new (self-hosting) compiler for Miranda, with additional features from Haskell and other functional languages:

https://github.com/taolson/Miranda2

and have updated the examples with David Turner's original "sieve" implementation.

any chance of expanding on doc/Language.md?
Yes, I plan to get to that; I'm currently working on documenting the compiler. I might put a pointer to existing documentation on Miranda there, as a placeholder in the meantime.
[edit to add]: There are also hundreds of small example programs of using Miranda2 to solve Advent of Code puzzles, here:

https://github.com/taolson/advent-of-code

Advent of Code Puzzle Descriptions can be found here:

https://adventofcode.com/

While they don't have the puzzle-supplied data sets included, they can be used to see how various solutions are written in Miranda2.

The author and editor should be ashamed for leaving out O’Neill from the title.
(comment deleted)
> Turner said that he was “interested in finding something simpler” than full dependent types.

What are some current options for avoiding full dependent types?

Lagniappe:

https://youtu.be/KBzlkPS7ZUw

https://arxiv.org/abs/1909.04628

>replace any theory which does not explain symmetrical observational situations as the manifestation of deeper symmetries

now I'd like to see Cambrian knot-fish!

is there a slogan for how Spekkens' metaphysics (epistemology?) differs from "working up to isomorphism"?

(we prefer theories which result from applying condensation to situations in order to form DAGs? minimise strongly connected components?)

Not that I know of but maybe! Let me know if you see/come up with one (edit: did you mean "homomorphism"?)

The trick to getting yt to return nonLatin recs seems to be: keep only high quality not-dubbed comedy in history..

Edit: maybe he should panned the cam

https://youtube.com/shorts/TWLZMVSbi6c

(What do you mean by "condensation"?)