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

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

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*.