3 ms·
If you want to prove your Lisp, you can always boot up ACL2. It was used (for example) to formally verify Buchberger's algorithm: <https://www.sciencedirect.co
by tmtvl 3y ago
If you want to prove your Lisp, you can always boot up ACL2. It was used (for example) to formally verify Buchberger's algorithm: <https://www.sciencedirect.com/science/article/pii/S0747717109001357 https://www.sciencedirect.com/science/article/pii/S074771710...>
- bella001 3y ago[dead]
- WanderPanda 3y agoHow do you even prove a language? I can't even imagine how that would work. Do you maybe have a pointer on where this rabbit hole starts? The one you provided seems more like a deep pocket than an entrance
- reikonomusha 3y agoYou would aim to prove properties of the formal semantics of a language, but that requires the language be described in a formal manner. Check out "The Definition of Standard ML" to get a sense of what a (mostly kosher) formal programming language definition might look like.