SPJ left Microsoft a couple of years ago but I don't remember what he is doing now. Does he still develop GHC?
I wonder what he thinks of:
-
The idea of using AI for automatic code synthesis in dependently typed languages. The idea is that if the (human-written) types are precise enough and the code is effect-free, you avoid the hallucinations and other issues with current LLM-generated slop/code. Of course being able to generate code with an arbitrary type amounts fo AGI-level automated reasoning, but it's ok to accept limitations on how powerful it can be.
-
Whether Haskell itself still excites him and if not, what does. Does he like Idris? Maybe Lean? And on the low level effectful side, what about Rust? What does he think are the current exciting ideas in PLT (programming language theory), and for that matter in general?
-
Is he familiar with Ben Lippmeier's dissertation about Discus, formerly called the Disciplined Disciple Compiler (DDC)? It had a very interesting critique[1] of Haskell in its first chapter, that motivated the DDC language design, that used effect types to track memory mutation. The language never caught on and might not have really been usable, but the motivation for it seemed mostly valid to me. So I wondered if Haskell has any answers to that section of the thesis.
[1] https://benl.ouroborus.net/papers/2010-impure/lippmeier-impure-world.pdf start at page 17.
I may think of some other things to add.