Re:Software correctness is a lot like flossing (2020)
by rotifer on Friday February 04, 2022 @12:19AM
(#30203186)
That's what TDD seems to mean to Edwin Brady, whose book is "Type-Driven Development with Idris" [1].
Idris [2] is a Haskell-like language, but unlike Haskell it's strict and from the beginning was designed around a dependent type system. (Types and values exist on the same level, so that types can include values, be passed as arguments to functions, and be returned by functions.)
In the book Brady encourages you to create the skeleton of a function, then leverage the type system to help flesh it out.
Idris [2] is a Haskell-like language, but unlike Haskell it's strict and from the beginning was designed around a dependent type system. (Types and values exist on the same level, so that types can include values, be passed as arguments to functions, and be returned by functions.)
In the book Brady encourages you to create the skeleton of a function, then leverage the type system to help flesh it out.
[1] https://www.manning.com/books/type-driven-development-with-i...
[2] https://www.idris-lang.org/index.html