We need special "prover benchmarks" for the proof assistants. I.e. write proof of the same proposition and time how long it takes for them to verify it.
Name:
Anonymous2014-12-07 15:25
Can these proof assistants also be used as general purpose programming languages?
Name:
Anonymous2014-12-07 15:32
>>3 If you love BDSM so much that C++ isn't enough, then yeah, they can.
Idris is the only one of those at least remotely reminiscent of a real language. The Chicken and the Cock are, well, just provers. You don't run 'em, you typecheck 'em.
Name:
Anonymous2014-12-07 15:37
>>3 Agda can but not really. A hello world takes 20 MB.
Agda is like, the assembly of linguistics: you can do anything with it, but you start from nothing, or maybe, even less than nothing.. since you must define ``nothing'' first