iiinova — where your digital self keeps evolving

Reposted by Type Theory Forall

Alcides Fonseca @handle.invalid · 11/09/2026

How to adapt CS degrees to AI? Here's my take: wiki.alcidesfonseca.com/blog/fall-20... looking for feedback from you.

wiki.alcidesfonseca.com

Fall 2026 Recommendations for AI in Higher Education by Alcides Fonseca

011

Type Theory Forall @ttforall.bsky.social · 10/09/2026

FLT formalized in Lean by AI Navier–Stokes attacked by AI, with the result formalized in Lean Autoformalization is moving fast Three years ago I interviewed Kevin Buzzard about his vision for mechanizing modern mathematics It might be time to revisit that conversation:

twp.ai

youtu.be

#26 Mechanizing Modern Mathematics - Kevin Buzzard

000

Type Theory Forall @ttforall.bsky.social · 05/09/2026

We also dive into Racket, programming language design, and Shriram’s decades of experience thinking about how we teach people to reason about programs. A fascinating conversation! ▶️ twp.ai/4hvacX 3/3

twp.ai

youtu.be

0205

Type Theory Forall @ttforall.bsky.social · 05/09/2026

I sat down with @shriram.bsky.social to talk about PL education, how LLMs are changing the way students learn programming, and what we should actually be teaching when AI can increasingly write the code for us. 2/3

161

Type Theory Forall @ttforall.bsky.social · 05/09/2026

How should we teach Programming Languages in the age of AI? New TTFA episode! 🎙️ 1/3

171

Type Theory Forall @ttforall.bsky.social · 07/08/2026

This is fantastic news. A new effort is underway to produce a Revised Haskell 2010 Language Report—updating the language specification after 16 years while keeping a well-defined, implementable standard. twp.ai/9OZs47

040

Type Theory Forall @ttforall.bsky.social · 07/08/2026

We also discuss gradual typing, language design, reactive programming, and AI. 🎙️ twp.ai/9OZqsb 2/2

twp.ai

youtu.be

Hack: The Language that Fixes PHP

000

Type Theory Forall @ttforall.bsky.social · 07/08/2026

How do you add static types to one of the largest PHP codebases on the planet? I sat down with Julien Verlaguet, one of the creators of Hack, to hear the story behind one of the most ambitious language migration efforts ever attempted. 1/2

131

Type Theory Forall @ttforall.bsky.social · 15/06/2026

We talked about how GHC is developed, how the Haskell community decides to evolve the language, what it takes to start hacking on GHC, and then went deep into the theory and implementation of Dependent Haskell. This one gets technical in the best way. Watch here: twp.ai/4hsWdw 2/3

twp.ai

youtu.be

#62 - Dependent Haskell - Vladislav Zavialov

200

Type Theory Forall @ttforall.bsky.social · 15/06/2026

New Type Theory Forall episode is out! I had the pleasure to partner with @serokell to bring you a conversation with Vladislav Zavialov, one of the main GHC contributors, former GHC Steering Committee member, and current implementer of Dependent Haskell. 1/3

110

Type Theory Forall @ttforall.bsky.social · 02/06/2026

Past sponsors have included companies, research groups, conferences, and open-source projects. Feel free to reach out if you have any questions. And if you know someone who might be interested, a retweet would be greatly appreciated for reach. 3/3

000

Type Theory Forall @ttforall.bsky.social · 02/06/2026

If you'd like to promote your company, research project, open-source tool, conference, or community to an audience interested in programming languages, formal methods, theorem proving, and functional programming, you can commission an episode here: twp.ai/9OXQgJ 2/3

twp.ai

ko-fi.com

Type Theory Forall's Commissions are Open!

100

Type Theory Forall @ttforall.bsky.social · 02/06/2026

We have an opening in the Type Theory Forall schedule this month for a sponsored episode. 1/3

100

Reposted by Type Theory Forall

Jean Abou Samra @jeanas.bsky.social · 22/05/2026

The Budapest type theory group is hiring a postdoc to work on higher observational type theory. lists.seas.upenn.edu/pipermail/ty...

lists.seas.upenn.edu

[TYPES/announce] Postdoc position in type theory

045

Type Theory Forall @ttforall.bsky.social · 01/05/2026

The TTFA store is closing May 19. Last chance (for a while) to grab: PL mugs, shirts, hoodies, hats — plus the Tony Hoare tribute drop. twp.ai/9OUsKk After a year, we basically broke even — so going forward: • Open once a year • Next reopening: holidays Don’t miss this window.

000

Type Theory Forall @ttforall.bsky.social · 30/04/2026

The TTFA store is closing May 19. Last chance (for a while) to grab: PL mugs, shirts, hoodies, hats — plus the Tony Hoare tribute drop. twp.ai/9OUvqF After a year, we basically broke even — so going forward: • Open once a year • Next reopening: holidays Don’t miss this window.

000

Type Theory Forall @ttforall.bsky.social · 19/04/2026

Then we reopen only for the holidays If you’ve been thinking about getting something — now’s the time. Appreciate all the support ❤️ 2/2

010

Type Theory Forall @ttforall.bsky.social · 19/04/2026

Dropping 2 new items today in tribute to Tony Hoare: • C.A.R T-Shirt • Hoare Triple Hat A small way to celebrate someone who shaped how we think about programming and correctness. twp.ai/9OVSQV The store will now only open once a month ⏳ This drop closes May 19 1/2

120

Type Theory Forall @ttforall.bsky.social · 16/04/2026

New TTFA episode I sat down with Farhad Mehta, one of the main organizers of Zurihac, the largest Haskell event in the world. We talk about: • the story behind Zurihac • what it takes to run it • Farhad’s path across academia and industry Zurihac 2026: June 6–8 in Zurich

twp.ai

Type Theory Forall

Type Theory much beyond inference rules

052

Type Theory Forall @ttforall.bsky.social · 15/04/2026

The store will now only open once a month ⏳ This drop closes May 19 Then we reopen only for the holidays If you’ve been thinking about getting something — now’s the time. Appreciate all the support ❤️ 2/2

000

Type Theory Forall @ttforall.bsky.social · 15/04/2026

110

Reposted by Type Theory Forall

Cyrus Omar on sabbatical in Cambridge @neurocy.bsky.social · 10/04/2026

Ordered Agda and OCaml mugs from the @ttforall.bsky.social merch store and Pedro threw in a little bonus! 💚

three mugs, depicting the logos of Agda, OCaml, and Hazel, sitting on office desk

2274

Reposted by Type Theory Forall

aron @adler.dev · 27/03/2026

men are from Type, women are from Prop

4304

Type Theory Forall @ttforall.bsky.social · 27/03/2026

You can get access to the video through the System F tier for $5 using the discount code DFC5C. twp.ai/9PcpYA 4/4

twp.ai

www.patreon.com

Patreon

000

Type Theory Forall @ttforall.bsky.social · 27/03/2026

I confess that this is not a super well polished video, but if you like foundational papers discussion, I think you'll enjoy this. To share this with a slightly broader audience, I’m offering 50% off the first month on Patreon. 3/4

100

Type Theory Forall @ttforall.bsky.social · 27/03/2026

The first episode is out now, and it’s on Frege, centered around his essay “The Thought: A Logical Inquiry.” I think it's a fascinating entry point into how these foundational ideas started to take shape. 2/4

100

Type Theory Forall @ttforall.bsky.social · 27/03/2026

Hey everyone! I’ve just started a short series for Patreons where I study and discuss the story of the logicians that make up the intuitionistic lineage. I'm trying to connect the people, ideas, and historical context in a more linear narrative. 1/4

100

Type Theory Forall @ttforall.bsky.social · 25/03/2026

New TTFA episode 🎙️ What does it mean to build a research career today? With Dan Plyukhin we talk about: • meditation & staying sane • the reality of the job market • reaching out to professors • AI (hype vs reality) • research paths

twp.ai

www.youtube.com

#60 - Conversations on Life, AI, and the PL Job Market - Pedro and Dan

000

Type Theory Forall @ttforall.bsky.social · 24/03/2026

“The thought, in itself immaterial, clothes itself in the material garment of a sentence and thereby becomes comprehensible to us” — Frege 1956

010

Type Theory Forall @ttforall.bsky.social · 18/03/2026

Tristan Stérin used LLMs to hunt for bugs and inconsistencies in Rocq and Lean. This is actually pretty neat and kind of wild.

twp.ai

tristan.st

Tristan Stérin

010

Type Theory Forall @ttforall.bsky.social · 16/03/2026

Few researchers have shaped the intellectual foundations of our field so deeply. Thank you, Tony Hoare. May you rest in peace. 7/7

010

Type Theory Forall @ttforall.bsky.social · 16/03/2026

Hoare also introduced null references in ALGOL W, which he later called his “billion-dollar mistake,” a candid reflection that pushed language designers toward safer type systems. For these and many other contributions he received the ACM Turing Award in 1980. 6/7

110

Type Theory Forall @ttforall.bsky.social · 16/03/2026

He also created Communicating Sequential Processes (CSP), a foundational model for concurrency and message-passing systems that influenced languages and systems for decades. 5/7

110

Type Theory Forall @ttforall.bsky.social · 16/03/2026

In 1969 he introduced Hoare Logic in An Axiomatic Basis for Computer Programming, giving us the famous Hoare triple {P} C {Q} and launching the field of formal reasoning about programs. 4/7

110

Type Theory Forall @ttforall.bsky.social · 16/03/2026

His first idea was insertion sort, but this line of thinking led him to invent Quicksort — still one of the most widely used sorting algorithms in the world. 3/7

110

Type Theory Forall @ttforall.bsky.social · 16/03/2026

In 1960, while a visiting student at Moscow State University working on a machine translation project, Hoare needed a way to sort the words of Russian sentences before looking them up in a Russian–English dictionary. 2/7

120

Type Theory Forall @ttforall.bsky.social · 16/03/2026

Today we honor the life and work of Sir Tony Hoare (1934–2026), one of the giants of computer science. His work shaped algorithms, programming languages, concurrency, and formal verification. 1/7

251

Type Theory Forall @ttforall.bsky.social · 08/03/2026

Some people drink coffee. Others drink coffee and reason about it formally ☕ FP & proof assistant mugs → twp.ai/9Pb5eO

000

Type Theory Forall @ttforall.bsky.social · 06/03/2026

Some people drink coffee. Others drink coffee and reason about it formally ☕ FP & proof assistant mugs → twp.ai/9PatXs

012

Type Theory Forall @ttforall.bsky.social · 04/03/2026

Some people drink coffee. Others drink coffee and reason about it formally ☕ FP & proof assistant mugs → twp.ai/9Pay3E

010

Type Theory Forall @ttforall.bsky.social · 02/03/2026

Some people drink coffee. Others drink coffee and reason about it formally ☕ FP & proof assistant mugs → twp.ai/9Payr1

010

Type Theory Forall @ttforall.bsky.social · 24/02/2026

For students and engineers working in PL, compilers, or formal verification, understanding these three perspectives is essential. They are not competing views. They are complementary lenses on what programs are and what it means for them to be correct. 8/8

000

Type Theory Forall @ttforall.bsky.social · 24/02/2026

This tradition gave us foundational ideas such as invariants and Hoare logic, emphasizing reasoning as central to programming. Operational semantics models execution. Denotational semantics models mathematical meaning. Axiomatic semantics models provability. 7/8

100