rigille
Re:Show HN: High-order Virtual Machine (HVM) – A Parallel Functional R...
on Monday January 31, 2022 @07:44PM (#30157086)
I honestly can't believe I'm having the chance to contribute with this right from the start
Re:Kind: A Modern Proof Language
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
on Wednesday August 11, 2021 @01:39PM (#28145123)
Thanks for pointing that out! It's now fixed.
Re:Kind: A Modern Proof Language
on Wednesday August 11, 2021 @12:39PM (#28144325)
That's a great idea. Kind for example compiles to a small core language called FormCore which can be typechecked with 700 lines of javascript. In theory other languages could compile to FormCore and have good interoperability with Kind.