undefined | Better HN

0 pointsolliesaunders13y ago0 comments

Why wouldn’t you use it Agda/Coq for general development? (Looking for reasons other than a presumed lack of libraries.)

0 comments

It's very slow and every function must have formal properties, e.g. all functions are total and must formally be proved to terminate.

(As far as I know. I've only worked through Pierce's book.)

j / k navigate · click thread line to collapse

0 pointsolliesaunders13y ago0 comments

Why wouldn’t you use it Agda/Coq for general development? (Looking for reasons other than a presumed lack of libraries.)

It's very slow and every function must have formal properties, e.g. all functions are total and must formally be proved to terminate.

(As far as I know. I've only worked through Pierce's book.)

j / k navigate · click thread line to collapse