# AI tooling for types and effects

Every method in this family has a checker that can refuse the answer, so
AI proposes and the compiler or the solver decides. The field moves
quickly, and these entries may be out of date.

## Type systems

General coding assistants (Copilot, Cursor, Claude Code, Aider)
are the de-facto workflow for type completion and JS→TS /
Python→[mypy](https://github.com/python/mypy) migration. **TypeT5** (Wei et al. 2023)[^wei2023] infers
Python types and beats the earlier HiTyper / Type4Py line. The
checker's guarantee stops at shape: annotations that type-check
are frequently wrong about intent (Yee and Guha 2023)[^yee2023].

## Linear types

`rustc` with an LLM in the loop is the de-facto workflow: the
compiler is the oracle, so AI cannot ship a memory-unsafe
program without writing `unsafe`. C→Rust translation at scale
is active research — DARPA's [TRACTOR program](https://www.darpa.mil/research/programs/translating-all-c-to-rust)
and LLM-repair extensions to the classical C2Rust pipeline.

## Refinement and dependent types

The SMT solver is the oracle. **Laurel** (Mugnier et al. 2025)[^mugnier2025] writes the
helper assertions a failing proof needs, and **Clover** (Sun et al. 2023)[^sun2023]
checks a function against its docstring and its annotations; both
target [Dafny](https://dafny.org/). **AutoSpec** (Wen et al. 2024)[^wen2024] and **SpecGen**
(Ma et al. 2024)[^ma2024] target C/Java spec generation.

## Effect systems

No AI tool proposes effect annotations: [Koka](https://koka-lang.github.io/koka/doc/index.html),
[Eff](https://www.eff-lang.org/) and [Unison](https://www.unison-lang.org/) are small enough that a
model sees little of their code in training.

## References

[^wei2023]: Wei, Jiayi, Greg Durrett, and Isil Dillig. 2023. *[TypeT5: Seq2seq Type Inference using Static Analysis](https://arxiv.org/pdf/2303.09564)*. <https://doi.org/10.48550/arXiv.2303.09564>.
[^yee2023]: Yee, Ming-Ho, and Arjun Guha. 2023. "[Do Machine Learning Models Produce TypeScript Types That Type Check?](https://arxiv.org/pdf/2302.12163)" *Proceedings of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)*. <https://doi.org/10.48550/arXiv.2302.12163>.
[^mugnier2025]: Mugnier, Eric, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. 2025. "[Laurel: Unblocking Automated Verification with Large Language Models](https://arxiv.org/pdf/2405.16792)." *Proceedings of the ACM on Programming Languages*, 1519–45. <https://doi.org/10.1145/3720499>.
[^sun2023]: Sun, Chuyue, Ying Sheng, Oded Padon, and Clark Barrett. 2023. *[Clover: Closed-Loop Verifiable Code Generation](https://arxiv.org/pdf/2310.17807)*. <https://doi.org/10.48550/arXiv.2310.17807>.
[^wen2024]: Wen, Cheng, Jialun Cao, Jie Su, et al. 2024. "[Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://link.springer.com/content/pdf/10.1007/978-3-031-65630-9_16.pdf)." *Formal Methods for Software Engineering (SEFM 2024)*, Lecture notes in computer science, 302–28. [https://doi.org/10.1007/978-3-031-65630-9\\\_16](https://doi.org/10.1007/978-3-031-65630-9\_16).
[^ma2024]: Ma, Lezhi, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2024. *[SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://arxiv.org/pdf/2401.08807)*. <https://doi.org/10.48550/arXiv.2401.08807>.

## Acronyms

- SMT — satisfiability modulo theories