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$

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