3 ms·
> If we take 'specifications' one level further and actually want our algorithms to be proven correct, as in, by a proof assistant it is quite unclear that this
by rntz 7y ago
> If we take 'specifications' one level further and actually want our algorithms to be proven correct, as in, by a proof assistant it is quite unclear that this possible or desirable.
It is not only possible, it is how dependently-typed languages/proof-checkers like Agda work.
- cjfd 7y agoThe question is whether the performance hit that one gets from running such a language at run time is acceptable. For one, thing, it pretty much forces one to use a purely functional language. Which may or may not be a good thing.