Simple to Use Proofs and Program Verification
sirinath opened this issue · 1 comments
sirinath commented
Can simple to use proofs be added to the language in the spirit of Formality, ATS Programming Language, Why3/WhyML, Whiley, SPARK or Dafny.
slightknack commented
Potentially in the future, but this isn't the main use-case for Passerine, and the type system hasn't been fully implemented yet. I'm closing this issue for now; once we're reached the point where proofs may be possible, consider re-opening it :)