you could have mix of assertions and proofs, obtaining something that you could call gradual verification - you wouldn't have to prove everything from axioms, you could base on assertions.
the difference from asserts and unit testing is that you could match post-contract from one function with pre-contract of another one, as in:
fun sort(l: List[Int]): SortedList[Int]
fun minusReverse(l: SortedList[Int]): SortedList[Int] = l.map(el => -el)
fun f(l: List[Int]): SortedList[Int] = minusReverse(sort(l))
when you have sort and minusReverse functions unit-tested, you could use proof system to prove that f is correct (assuming that sort and minusReverse are).
while looking for similar concepts in existing programming languages I have found that SPARK 2014 [1] (subset of Ada 2012 with static verification) follows such philosophy: you can prove some parts of the code and unit test the rest.
the difference from asserts and unit testing is that you could match post-contract from one function with pre-contract of another one, as in:
fun sort(l: List[Int]): SortedList[Int]
fun minusReverse(l: SortedList[Int]): SortedList[Int] = l.map(el => -el)
fun f(l: List[Int]): SortedList[Int] = minusReverse(sort(l))
when you have sort and minusReverse functions unit-tested, you could use proof system to prove that f is correct (assuming that sort and minusReverse are).
while looking for similar concepts in existing programming languages I have found that SPARK 2014 [1] (subset of Ada 2012 with static verification) follows such philosophy: you can prove some parts of the code and unit test the rest.
[1] https://www.adacore.com/about-spark
[2] http://docs.adacore.com/spark2014-docs/html/lrm/introduction...