Scala vs Idris - Dependent Types, Now and in the Future

This course explores the comparison between Scala and Idris in terms of their dependent types, focusing on the present and future possibilities. The learning outcomes include understanding the power of type systems, especially dependent types, and their role in program verification. Participants will gain insights into the expressive capabilities of Scala's type system and the advanced features of Idris, such as full spectrum dependent types and theorem proving. The course aims to showcase the potential of modern type systems through practical examples, discuss current limitations, and speculate on the future advancements in languages with full dependent types. The intended audience for this course includes programmers interested in functional programming, type systems, and program verification techniques. The teaching method involves a presentation format with demonstrations and examples provided by the instructors.