3 ms·
In the dependently typed family of languages it's a little bit arbitrary to divide between programming languages and proof assistants since everyone in this spa
by omaranto 15y ago
In the dependently typed family of languages it's a little bit arbitrary to divide between programming languages and proof assistants since everyone in this space can be made to play both roles in a pinch. I think most people think of Coq as more on the proof assistant side and Agda more on the programming language side.
- Locke1689 15y agoSort of. Dependent types doesn't explain Coq's requirement for pure, total functions. Unless this restriction is weakened I cannot see it as being useful in any general-purpose domain. Agda may be looser.
- DanWaterworth 15y ago> Dependent types doesn't explain Coq's requirement for pure, total functions. That's where you are wrong. Partial functions introduce the bottom value and then you can 'prove' arbitrary incorrect things.
- Locke1689 15y agoI'm not sure what you're saying. I was saying that simply being dependently typed doesn't necessitate pure total functions. Obviously, these features can be considered either highly suggested or necessary for ITPs. There are a number of ways you can get around totality with dependent types.