Lambda World is a conference aiming to scale the usage of the research achievements in the area of functional programming over the last 40 years in the industrial setting. Aleks Nanevski and Anton Trunov have tried to push it even further, showcasing modern technology, like proof assistants, built on top of dependent types. This approach is highly desirable in the branches of industry needing high assurance guarantees. Anton delivered a workshop on programming in Coq aiming at software developers. And Aleks presented a talk on proof automation using Coq’s canonical structures.