Am I arrogant? It's too soon to tell!
16.01.2025 20:06 — 👍 1 🔁 0 💬 0 📌 0@barryjay.bsky.social
A retired prof who tries to get some research in before cycling with the bunch at dawn. I like my work to surprise people, but am now so radical that few believe me, even though all theorems in my second book “Tree Calculus” are formally verified.
Am I arrogant? It's too soon to tell!
16.01.2025 20:06 — 👍 1 🔁 0 💬 0 📌 0Counting the real numbers in tree calculus
06.01.2025 06:42 — 👍 2 🔁 0 💬 0 📌 0Type inference is hard but don't hack the terms, just the types: the correct link is
04.01.2025 21:41 — 👍 2 🔁 0 💬 0 📌 0Oops! Will fix in half-an-hour
04.01.2025 21:28 — 👍 0 🔁 0 💬 0 📌 0Type inference is hard but don't hack the terms, just the types
04.01.2025 20:20 — 👍 3 🔁 0 💬 2 📌 0The semantics-syntax distinction is just code for the mind-body problem
03.01.2025 23:14 — 👍 3 🔁 1 💬 0 📌 0New Year's resolutions are out! My watchword for 2025 is **fun**
30.12.2024 20:35 — 👍 0 🔁 0 💬 2 📌 0Anzac Bridge on Sydney Harbour from my balcony with thermal underwear packets on the table, reflections of the building in the glass of the balcony wall
Sunny Sydney to freezing Denver, I’m ready to go with my Christmas woollens
24.12.2024 20:38 — 👍 2 🔁 0 💬 0 📌 0Logic engineers truth.
14.12.2024 01:12 — 👍 1 🔁 0 💬 0 📌 0If you are going to POPL 2025 in Denver consider coming to my talk at #PEPM2025 on the missing diagonal.
The computing community has produced many high level languages and tools for programming high level systems (e.g. Java for user interfaces)
popl25.sigplan.org/details/pepm...
My 15 minutes of fame as #1 on HackerNews GitHub.com/barry-jay-personal/blog/blob/main/2024-12-13-fame.md
12.12.2024 20:19 — 👍 4 🔁 0 💬 0 📌 0Neo-gothic? Sandstone church viewed up through some trees, two stained glass windows, some ferns on the slope
Lavender Bay then Luna Park, seen from behind in foreground then half of Sydney Harbour Bridge framing one shell of the Opera House
The view of, and from Christ Church, Lavender Bay
12.12.2024 20:09 — 👍 1 🔁 0 💬 0 📌 0Calculus or Calculi? at GitHub.com/barry-jay-personal/blog/2024-12-12-calculus-calculi.md explains why there are now two versions of tree calculus in play, and that’s ok
11.12.2024 23:37 — 👍 2 🔁 0 💬 0 📌 0Since some people find my writing too dense, I’ve written a blog “Turning Poetry into Prose” to expand on my new paper “Typed Program Analysis without Encodings” that shows how to type my tree calculus. The blog, paper and book are all at GitHub.com/barry-jay-personal/
10.12.2024 10:14 — 👍 3 🔁 0 💬 0 📌 0Right! You can also check out my book “Reflective Programs in Tree Calculus” and a type theory for it “Typed Program Analysis without Encodings” at GitHub.com/barry-jay-personal
10.12.2024 05:14 — 👍 4 🔁 0 💬 1 📌 0So, this is cool:
treecalcul.us
A very simple intensional calculus. A simple, privileged programming language where functions can be analyzed, serialized, etc.
The interesting meaning of “blatant” is “open and shameless”. Since “blatant” is degraded, perhaps we just use “open and shameless” instead, or “shameless” where “open” is understood.
09.12.2024 23:16 — 👍 0 🔁 0 💬 0 📌 0Glass tabletop with painted-dessert coffee cups and water glasses over a mirror supporting a circle of rocks in purple, blue and shiny gold
Breakfast coffee on a table of fools gold
28.11.2024 21:05 — 👍 0 🔁 0 💬 0 📌 0A small, shingle boathouse, framed by branches on the other side of the lake
An open shelter, with a modern sloped roof supported by twelve pillars made of tree trunks with stubs of branches providing triple support
Working from home: Crater Lake or Cataract Gorge?
26.11.2024 07:13 — 👍 1 🔁 0 💬 0 📌 0Rustic path leading off to the left; cradle Mountain framed by a blue sky above; on the right, a two metre tall grass (dead leaves hanging down, a crown of green spikes)
Walking around Dove Lake, under Cradle Mountain, Tasmania
24.11.2024 21:44 — 👍 2 🔁 0 💬 0 📌 0It’s like a simmering pot of water: the hotter it gets, the more it roils
21.11.2024 03:00 — 👍 2 🔁 0 💬 0 📌 0My paper “Typed Program Analysis without Encodings” has been accepted for PEPM (a satellite meeting of POPL) in Denver in January. It shows how to type tree calculus, including its self-interpreters. If you’re going I’d be happy to meet up!
19.11.2024 05:48 — 👍 3 🔁 0 💬 0 📌 0Nested steel shells in lieu of the old rotunda in the park
Railway tracks and power lines create a forced perspective that cradles a row of unusually straight eucalypts
Shapes from today’s walk
18.11.2024 05:02 — 👍 1 🔁 0 💬 0 📌 0Hooray, a one-way street in #Sydney becomes two way for #bicycles (and brush turkeys)
14.11.2024 23:23 — 👍 3 🔁 0 💬 0 📌 0