we-assert and automated proofs

I have a tiny javascript package I wrote for internally verifying javascript. It’s called “we-assert”, available on GitHub at xerocross/we-assert. Right now it does a few very basic things, but I wouldn’t really recommend anyone else use it yet.

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 xerocross.vulcan.

Vulcan can prove simple propositions. If you assume "A" and "A -> B" then it can verify a proof of "B". I spent most of today thinking about whether you can use this along with an assertion tool like we-assert to make scripts that are self-proving. Actually, I think “self-proving” is far too grandiose a phrase. Instead, I will just say I want to be able to write JavaScript functions so that if I include intelligent assertion statements then the output is verified automatically when you execute the function.

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.