I've been thrashing around with agda (as a hobby) for a few months. Maybe it's time to take lean for a spin.
My thinking is still pretty fuzzy. But I feel like there's something important and valuable with the idea of "this is the specification of the software" and the "this software meets that specification".
Now, yes, maybe the specification is wrong. Proofs are hard to write. All software has a bunch of implicit constraints. I forget them for the code I wrote, and it's even tougher to figure them out when I'm handed a legacy project where the author is long gone.
There's something really important about that dual view of, this is what it's supposed to do, and this is what it does. And tools can help check that they agree!
There's like the classic Haskell example of verified email - at some point the user was sent an email and they clicked a link, so that string is special, pretty sure foo@example.com is a real email.
The ability to slap a type on something, then have tools tell you "this is everything that needs to be updated" is really appealing. Like, The account must be in good standing before shipping product. So I keep puttering around with it.
It's often difficult to add features and be super sure you're not breaking stuff. Well, maybe not you, but me, for sure.
> There's something really important about that dual view of, this is what it's supposed to do, and this is what it does. And tools can help check that they agree!
Isn’t this the whole concept behind writing tests?
It is! And I'm a big fan of test systems that optionally invert the logic and require failure - to weed out bullshit tests.
But there are some things that are challenging to test for. Tests sample the space, proofs define the space. you can't build it wrong. (you can sure have a bad spec, and build the wrong thing though)
Tests definitely help. It sorta feels like there's value left on the table. The spec, the types let you define broader constraints, and you catch them all.
I'm one of the people who believe that TDD and safety-by-design (which is based on strong, static typing) are actually two sides of the same coin. In a sufficiently powerful type system, they could possibly even be two implementations of the same thing.
- Start with spec.
- Write the specs as something that the compiler/test harness will check for you.
- Write the code.
The main differences being, of course, that you'll typically get your compiler error messages much faster than your test error messages (typically while you're writing the code), which makes them easier to fix - on the other hand, in pretty much all languages, the type system isn't expressive enough to represent all the specs that can be represented as tests.
In other words, in the current state of the world, we need both.
They're attacking the problem from two directions - bottom up and top down.
I view the type system as a way to whittle down the state space to the bare minimum while the tests validate that that the behavior of that whittled down execution space matches what is required.
I think investment in a type system to replace tests very quickly reaches a point of diminishing returns and vice versa. A really good type system won't ever beat ok tests + an ok type system and vice versa.
I’d like to see one of these systems designed around generating test suites for the specification. So, you’d prove your algorithm correct using some inefficient representation (nats for integers or whatever) and then the verifier would detect edge cases and generate a junit test suite for the real implementation.
My thinking is still pretty fuzzy. But I feel like there's something important and valuable with the idea of "this is the specification of the software" and the "this software meets that specification".
Now, yes, maybe the specification is wrong. Proofs are hard to write. All software has a bunch of implicit constraints. I forget them for the code I wrote, and it's even tougher to figure them out when I'm handed a legacy project where the author is long gone.
There's something really important about that dual view of, this is what it's supposed to do, and this is what it does. And tools can help check that they agree!
There's like the classic Haskell example of verified email - at some point the user was sent an email and they clicked a link, so that string is special, pretty sure foo@example.com is a real email.
The ability to slap a type on something, then have tools tell you "this is everything that needs to be updated" is really appealing. Like, The account must be in good standing before shipping product. So I keep puttering around with it.
It's often difficult to add features and be super sure you're not breaking stuff. Well, maybe not you, but me, for sure.