🇨🇦 Joey Eremondi

If you would like to know more about the projects, feel free to contact me (email address can be found at eremondi.com)

Embark on a Global Research Journey with Globalink Internship Join Mitacs Globalink Research Internship for Students. Expand your academic horizons with international research experiences.

Full eligibility requirements are at: www.mitacs.ca/our-programs...

Interested students can apply at globalink.mitacs.ca#/student/app... . Students can express interest in multiple projects and rank them according to preference.

Eligibility:

* Undergrad from one of: Brazil, Chile, China, Colombia, France, Germany, Hong Kong, Jordan, Mexico, Pakistan, Singapore, South Korea, Taiwan, Thailand, Tunisia, Ukraine, United Kingdom and the United States
* 1-3 semesters left in your program in Fall 2026
* Studying CS or math

I have three MITACS projects which are looking for undergraduate interns to work on:

* Flexible Pattern Matching in Dependently Typed Languages
* A Corpus of Error Messages from Dependently Typed Compilers
* Implementing Gradual Dependent Types in Idris or Lean

Summer Undergraduate Internship - reposts welcome!

Are you a senior undergrad, interested in Programming Languages? Do you want to visit Canada for a paid 12-week internship?

LLMs are great.

A little sent by this "proof" of P = NP that incorporates Lean, as if that helped in the least. Maybe it does! But... not much.

zenodo.org/records/1609...

A tweet from BBC News (UK) reads: "Monkeys will never type Shakespeare, study finds." Below the tweet is an image of a chimpanzee dressed in a button-up shirt and wearing glasses, sitting at a modern desk and typing on a laptop, mimicking a human office worker. A caption on the image says, "'Infinite monkey theorem' challenged by Australian math..." Underneath the tweet, a community context note clarifies: "Infinite monkey theorem talks about infinite monkeys over infinite time. This study talks about finite amount of monkeys over finite amount of time."

Memories

From the OpenAI community on Reddit Explore this post and more from the OpenAI community

This is fascinating: www.reddit.com/r/OpenAI/s/I...

Someone “worked on a book with ChatGPT” for weeks and then sought help on Reddit when they couldn’t download the file. Redditors helped them realized ChatGPT had just been roleplaying/lying and there was no file/book…

Incredibly grateful to @sigplan.bsky.social and @sigplan-pldi.bsky.social for awarding #LeanLang the Programming Languages Software Award 2025 at #PLDI2025!

#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics #SoftwareVerification

I like how explicit How To Design Programs is about the process that takes place in my head but that I never named.

"IDK all the details right now but this function surely will access the three numbers in the input list. Put those accesses in there surrounded with ..., deal with the rest later"

PhD and MSc students interested in Theorem Proving or Evolutionary Computation can apply for a Species scholarship to visit and collaborate with me in lisbon: wiki.alcidesfonseca.com/research/tea...

multiple audience members too young to remember Spectre/Meltdown holy shit time to order my own coffin

it is impossible to generate code comments from source code because good comments are definitionally based on things not in the source code (intent, counterfactuals, experiments, etc.)

I already hinted at it a few times. I’m building a new development environment for macOS. The current focus is on Haskell support, but it can also do Agda & Swift. I only just started beta testing with external testers, so there are still rough edges. Interested in giving the beta a spin? Send a DM!

oxcaml.org

HOMEWORK MACHINE The Homework Machine, oh the Homework Machine Most perfect contraption that's ever been seen. Just put in your homework, then drop in a dime, Snap on the switch, and in ten seconds' time, Your homework comes out, quick and clean as can be. Here it is — "nine plus four?" and the answer is "three." Three? Oh me ... I guess it's not as perfect As I thought it would be.

shel silverstein on the LLM, 1981

The more I learn about atmospheric chemistry, the more terrified and angry I am about satellite companies' blatant lack of consideration for how their actions will harm the atmosphere. I hope this gets a lot of press. Great work by a whole team of scientists, including @astrokiwi.bsky.social! […]

To show the absence of bugs you need a proof that works for all inputs. Failing the proof doesn't necessarily give you insight into WHAT input is wrong, or even if there is a wrong input at all! While a failing test guarantees you know at least one buggy input.

Right, but you're not really asking for reviewers, because it's not just review, it's *the actual hard interesting work of the project*

Right, but you are apparently either unwilling or unable to check the outcome of the experiment, while at the same time saying "This experiment was a success, as long as someone else does the work of verifying it was a success"

But the math holding is the only part that matters. You've asked an AI to build a car, and said "I haven't checked if it runs, but if it runs, look how amazing it is." You've done a pale imitation of the actual task, which is *checking if the math holds*.

Assistant Professor (Tenure-Track), Department of Computer Science The Department of Computer Science at the University of Regina invites applications for a tenure-track Assistant Professor in Cybersecurity or closely related area, starting January 1 or July 1, 2026....

Please share: my university is hiring a professor in Cybersecurity: urcareers.uregina.ca/postings/19339

Welp, in case we needed even more things to worry about, apparently in 3 days we're going to stress-test Starlink's current orbital configuration with a severe geomagnetic storm. After running simulations of Starlink's orbital configuration, I am honestly quite worried about how this is going to […]

Know C++, want to learn Rust? Read our new phrasebook teaching you how to convert C++ into Rust! (Work in progress, use our survey to tell us what you'd like to read about next!)
cel.cs.brown.edu/crp/

I have published my first new blog post in four years lexi-lambda.github.io/blog/2025/05...

It would be nice if more people understood Rice's Theorem

🚀 I'll be launching the Formal Methods Engineering Lab (manchester-fme.github.io) – and I am hiring!
If you’re interested, feel free to reach out.

“If I were a science journalist writing an article about a supposedly shocking development like this, I would email some experts and check to see if it’s for real. But plenty of science journalists don’t bother with that anymore: they just believe the press releases.”