I’d like to see one of these systems designed around generating test suites for ...

		fiddlerwoaroof on Oct 28, 2023 \| parent \| context \| favorite \| on: Can the language of proof assistants be used for g... 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.

If you can build a simpler implementation just using random data can help a lot.