Timeline for Proof Assistants in OOP languages
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 21 at 2:52 | comment | added | Alex Nelson | "So it's not that proof assistant designers were like Let's design a programming language for our proof assistant." Well, actually, that's historically exactly what happened. Plus logic isn't Turing Complete, so it can't be a programming language... | |
| Feb 17 at 12:18 | comment | added | Kid A | I understand your point, but my question is that can I provide the same environment in an OOP language as well? because I want to develop an application that has PA as a part (not the whole) therefore it would be nice to be able to benefit from OOP structures as well. | |
| Feb 16 at 19:05 | comment | added | Jason Rute | I feel your answer mixes up the proof assistant language and the metalanguage that the proof assistant is written in. For type-theory-based PAs I agree there is a lot of similarities of design between the PA language and functional programming, and there is a tight connection between type theory, functional programming, and proofs. But I think the OP is asking about the metalanguage, not the language of the proof assistant. (Also, the CH isomorphism might be a bit of a misdirection. For example, HOL-Light also looks like functional programming but doesn’t use the CH isomorphism.) | |
| S Feb 16 at 16:52 | review | First answers | |||
| Feb 17 at 16:01 | |||||
| S Feb 16 at 16:52 | history | answered | Christopher King | CC BY-SA 4.0 |