Re:Software correctness is a lot like flossing (2020)
by exdsq on Thursday February 03, 2022 @11:32PM
(#30202900)
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.
[ Parent
| on HN ]
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.
[1] https://www.manning.com/books/type-driven-development-with-i...
Re:Software correctness is a lot like flossing (2020)
by eyelidlessness on Thursday February 03, 2022 @11:42PM
(#30202952)
This 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.