Show HN: Dependently typed language for proofs that you can implement in one day

Re:Show HN: Dependently typed language for proofs that you c... by Twirrim on Saturday October 02, 2021 @01:34AM (#28726229)

> Pompom language is so simple that you can implement it yourself just by looking in the source code (you can think that our language is the BASIC language of proof assistants).

    List
      | A :: ~ * ~> * => {(list A) :: |new |empty }. // A list is either a new or a empty constructor

Okay... BASIC is a high level language, and it's aimed at people who are not involved in sciences. If your goal is to have a high level syntax, and aiming it at people maybe outside of those with formal proof background, I think that's a big miss. The syntax is anything but BASIC, compounded by the choice of lisp.

[ Parent | on HN ]

Re:Show HN: Dependently typed language for proofs that you c... by caotic123 on Saturday October 02, 2021 @01:47AM (#28726281)

I think you misunderstood, I have just made an analogy with BASiC. BASIC is normally a language that students used to implement when they are dealing with compiler topics. The fact is because BASIC is simple to learn and implement in the universe of structural languages. So, what I am saying is that you can do the same thing with Pompom, but of course, aiming at people that have at least a little experience with functional programming and type systems.

[ Parent | on HN ]

Re:Show HN: Dependently typed language for proofs that you c... by tluyben2 on Saturday October 02, 2021 @01:50AM (#28726296)

It is nicely done; the implementation is indeed simple and easy to read! It hopefully will make more language implementors understand.

I guess comparing it to BASIC is not good as this is complex matter: languages like Idris that have a vastly more complex implementation but therefore also a nice (imho) syntax, are still hard for most without theoretical background (I was raised and educated by Dijkstra pupils so it was pounded into me from very young); I found The Little Typer a good read on the subject, but that might be impossible for people without background as well; I cannot really estimate that.

[ Parent | on HN ]

Re:Show HN: Dependently typed language for proofs that you c... by tluyben2 on Saturday October 02, 2021 @01:46AM (#28726275)

> the choice of lisp.

Where? No lisp here as far as I can see. Haskell you mean?

But this is BASIC and simple to follow (including the source code of the language) for people interested in type systems and languages, not for just anyway. If you scroll down you see then the calculus with the words simple as well. This means: for people interested in implementing this, it is a very simple implementation and that is correct indeed. Nice work!

[ Parent | on HN ]