Comment by espeed

One of the keys for me was the use of types. Typestate when functions mint witnesses that can only come from it and are required to proceed and newtypes where you use custom types instead of strings so the agent can't forget. You can also use it to force the agent to use the implementation rather than reinvent the wheel by simulating linear types. Types are a much smaller target to optimize and provide constraints that fail loudly at compile time. (https://news.ycombinator.com/item?id=49806799)