3 ms·
Very next sentence: The only systems which can beat it are theorem provers like Coq, and they are not general purpose programming languages (Morriset and the Y
by DanWaterworth 13y ago
Very next sentence:
The only systems which can beat it are theorem provers like Coq, and they are not general purpose programming languages (Morriset and the YNot team might disagree though!).
ATS is dependently typed and therefore falls under theorem provers.
- Dewie 13y agoATS is meant to be a general purpose programming language. The fact that you have a theorem proving subsystem is to aid in the programming/verification. Idris is another dependently typed prog. lang. that is intended for general purpose programming.
- jlouis 13y agoIdris was not on my radar in 2010 :)