News for hackers. Stuff that matters.
Re:Kind: A Modern Proof Language by anentropic on Wednesday August 11, 2021 @01:43PM (#28145183)
> If you like unit tests, you’ll love theorems. To learn more, check THEOREMS.md.

Can someone ELI5...

I quite like unit tests, but it's hard to connect proving bits of elementary maths like `1 != 0` to anything I do as a software developer. Not really clear why I should have to/want to.

Re:Kind: A Modern Proof Language by rigille on Wednesday August 11, 2021 @02:15PM (#28145608)
Unit tests are theorems too! When you compute `Test(x)` and check it's `true` you have proven the theorem `Test(x) == true`. However that's only about a specific choice of `x`. Theorems allow you to use math to test all choices of `x` and cover infinitely many test cases.

In theory you could even write an unit test and offer a bounty to the first to write a function that's proven to pass it. So you wouldn't need to write it or review the results for correctness.

Re:Kind: A Modern Proof Language by iammisc on Wednesday August 11, 2021 @01:47PM (#28145239)
What kinds of things do you unit test that aren't propositions?