4 ms·

But this was not magical: the code has to have a specific check coded in that verify that one thing added here is also added there... AKA a unit test? Sure it'

But this was not magical: the code has to have a specific check coded in that verify that one thing added here is also added there... AKA a unit test? Sure it's nice that the language itself has a built-in way to verify a complex invariant and not having to write a unit test. But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design. In some (C++) projects I've worked on, adding a new configuration item would automatically documents it because the class to create a configuration item requires you to provide a doc string argument. So it could be even less forgotten.

sourceless 6y ago
> having this kind of convenience let you be lazy about design Or, conversely, this kind of correctness by construction allows you to focus on parts of the program that could suffer from non-trivial bugs
Jtsummers 6y ago
> But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design. How does having this in the language permit laziness in design? You still have to think about the properties in order to describe them, whether it's going into a type system or a test suite. Does the laziness occur once the property is placed into the type system because you can now rely on the compiler to assist you? Wouldn't the same argument apply to having a test suite that detected similar failures to maintain these properties?
laserharvest 6y ago
> [Having and using dependent types] let[s] you be lazy about design. Now I’ve heard it all.
marcosdumay 6y ago
> AKA a unit test Hum... No. It's not a test. A test is some code that tries to detect the presence of errors with specific execution data and environment. This is verification, that is code that tries to detect the absence of errors over any possible execution data and environment. The distinction is extremely relevant, mostly because a little bit of validation can replace entire screens of tests, and because tests tend to become stale, while validations tend to be generic enough to survive refactoring and even changes in requirements. But well, I entirely agree with this: > But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design. It's very nice to hack some minimum proof of concept of the most relevant problems, and be able to refactor it into some high quality code just by setting the checks for quality and blindly following their results. I imagine that's also what the "TDD for everything" people like so much about their processes.
PoignardAzur 6y ago
It sounds like you had roughly the same setup as what the Tweet author describes, except you didn't need fancy typing features. Like, yeah, enforcing that env variables are accessed in a structured way is kind of a solved problem. I don't think dependent typing adds that much.

sourceless 6y ago

> having this kind of convenience let you be lazy about design Or, conversely, this kind of correctness by construction allows you to focus on parts of the program that could suffer from non-trivial bugs

Jtsummers 6y ago

> But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design. How does having this in the language permit laziness in design? You still have to think about the properties in order to describe them, whether it's going into a type system or a test suite. Does the laziness occur once the property is placed into the type system because you can now rely on the compiler to assist you? Wouldn't the same argument apply to having a test suite that detected similar failures to maintain these properties?

laserharvest 6y ago

> [Having and using dependent types] let[s] you be lazy about design. Now I’ve heard it all.

marcosdumay 6y ago

> AKA a unit test Hum... No. It's not a test. A test is some code that tries to detect the presence of errors with specific execution data and environment. This is verification, that is code that tries to detect the absence of errors over any possible execution data and environment. The distinction is extremely relevant, mostly because a little bit of validation can replace entire screens of tests, and because tests tend to become stale, while validations tend to be generic enough to survive refactoring and even changes in requirements. But well, I entirely agree with this: > But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design. It's very nice to hack some minimum proof of concept of the most relevant problems, and be able to refactor it into some high quality code just by setting the checks for quality and blindly following their results. I imagine that's also what the "TDD for everything" people like so much about their processes.

PoignardAzur 6y ago

It sounds like you had roughly the same setup as what the Tweet author describes, except you didn't need fancy typing features. Like, yeah, enforcing that env variables are accessed in a structured way is kind of a solved problem. I don't think dependent typing adds that much.