15
$\begingroup$

I started programming a Haskell-clone recently (source code).

After basic hindley-milner, problems start to arise. Implementation of data/codata statements seem to ensure my language is breaking up on every front.

At this point I seem to lack foundations for the language. System F introduces kinds, but would it be better to approach theorem provers and pick a different calculus as foundation?

Also looking for overall suggestions for this kind of a project.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Are you using "theorem provers" and "proof assistants" as synonyms? $\endgroup$
    – Andrej Bauer
    Commented Feb 9, 2022 at 22:03
  • $\begingroup$ Yes. I meant proof assistants. $\endgroup$
    – Cheery
    Commented Feb 10, 2022 at 10:39

2 Answers 2

Reset to default
12
$\begingroup$

If you are asking "can we use proof assistants to develop foundations of programming languages" then the answer is positive. Two well-known such developments are:

There are also specialized proof assistants that make it easier to develop the meta-theory of a programming language, such as Twelf, Abella and Beluga.

Improve this answer
$\endgroup$
2
  • $\begingroup$ edits should be at least 6 characters. weird... $\endgroup$
    – Dima Pasechnik
    Commented Feb 9, 2022 at 23:33
  • $\begingroup$ Fixed, thank you. $\endgroup$
    – Andrej Bauer
    Commented Feb 10, 2022 at 14:31
7
$\begingroup$

I'm interested in this application of theorem provers, but it's not my speciality. I can point you to Harper and Licata's paper Mechanizing Metatheory in a Logical Framework, which walks through using Twelf to prove results about a toy functional programming language.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.