I have been trying to wire we-assert together with an automated proof device. I found a simple one that I like for doing basic propositional logic. It’s called “vulcan” and it’s available on GitHub at RyanMarcus/vulcan. I had trouble with the associated npm package, and that repo has not been updated in 3 years, so I forked it. My fork is at xerocross/xerocross.vulcan. I didn’t change much really. So far I only tweaked the package file slightly and published it on npm under
Vulcan can prove simple propositions. If you assume
"A -> B" then it can verify a proof of
For example, to test whether a sorting algorithm has worked correctly, you can verify that the output is sorted. You can just directly check whether it is sorted after the algorithm has finished. But that isn’t very intelligent or desirable. A more desirable goal is to check that the actions performed on the data logically force the result to be a sorted list…somehow.
I don’t pretend to be the first person who ever thought of this. But I do know it’s not commonly done. I have never even seen it done in any of the languages I know. Which leads me to think about functional programming because there are tools built on functional programming languages for building programs that are also legitimate mathematical proofs. Perhaps I can learn something useful if I study Haskell. I happen to already own a book about Haskell, so that might be what I do right after I hit publish on this post.