I’ve been hacking on this side project for 7 months so I suppose it’s about time I wrote some tests… github.com/edwinb/Blodwen/
Conversation
Been following this repo for a while now. Very inspiring! And yes, tests would be most useful for those of us spectating 😂
1
1
I do have a fair few tests I’m running locally, but automating is always a good idea… just got a long way with types this time :)
1
1
Yeah, I'm getting a feeling that dependent types can get rid of the need of vast swaths of unit/integration tests, but you still need end-to-end tests to make sure you're on the right track.
2
1
Been kind of interested in the evolution of tests though... whether we can make the process of example tests, to property tests, to proofs smoother. Kind of would like to be able to say, write out a theorem then just dump on quickcheck if I don't have time to provide a proof…
Replying to
I’ve wondered about this too, but not very deeply. It’s probably achievable as an Idris library…
1
1
One tricky thing is that it is nice to be able to have examples at the term level, but then you are forced to run them all the time during type checking. Would be kind of cool if the typechecker interface looked more like a test-runner. I dunno 🤔
2
Show replies