3 ms·
It'd be nice if TDD started to mean 'Type-Driven Development' in the world of software correctness. I believe it's a much better way of writing, such that a pro
by exdsq 5y ago
It'd be nice if TDD started to mean 'Type-Driven Development' in the world of software correctness. I believe it's a much better way of writing, such that a project leveraging the type system in that way would be of better quality than a test-driven development project.
- eyelidlessness 5y agoThis is actually how I approach software development generally. I write the types as the first test(s). Despite claims to the contrary, this makes prototyping and experimenting really convenient, and I can use my type checker/IDE as a test runner without setting up any project config. It’s just… limited.
- rotifer 5y agoThat'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. [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i... [2] https://www.idris-lang.org/index.html https://www.idris-lang.org/index.html