Formally verified Idris backend

[jonas.cl]

Hello,

There is a formally verified compiler called PureCake, built on CakeML, that is a Haskell-like lazy functional language. Wouldn't it be fantastic if also Idris at one point could be a formally verified language, maybe by building a CakeML backend?

Then I was also wondering about the state of the last items in the "Things still missing" section in Idris2; cumulativity and rewrite? Any idea when those might be finished?

Kind regards

Jonas Claesson

https://cakeml.org/purecake/

Sent from ProtonMail, Swiss-based encrypted email.

[Dr. Jan Bessai]

Hi,

I think there are different design goals for different languages: Idris
(as far as I understands it) aims to make dependent types useful and
accessible for programmers. Its cousin Agda wants to be a lab for
exploring different type theories. Its second cousins Coq and Lean want
to be a great theorem provers with dependent types. Its distant relative
Isabelle does not embrace dependent types, but also wants to be a great
theorem prover.

Being formally verified until (and beyond) assembly language is a
property that is always welcome, but has more or less impact on / value
for the general goal of the language. I think for Idris the business
value for its overall goal is such that it would be nice to have, but
not necessarily if it requires fundamental changes to the compiler
architecture or slows development (e.g. by requiring to redo/adjust
formal verification whenever the language gets a new feature).

If I were to make a proposal for a PhD size project around Idris I'd
start with reading
https://blog.janestreet.com/oxidizing-ocaml-locality/

and asking if there is room for Idris with optional GC (perhaps even in
just parts of the program that need to run fast). I'd also ask if
dependent types (in particular building on those of Idris 2) would be
able to somehow push things described in the article back to the type
system. If Idris were to get non-gc rust/ocaml like performance while
being dependently typed and pleasant to use, that would be a huge win
for its overall goal.

Finally, non of this is not to discourage you from what you want to do.
If you want to try out building a formally verified Idris compiler, go
for it. Sometimes one just has to ignore what people say/think to make
progress. I'm also in no position to speak with any authority on pretty
much anything.

Bests,

Jan

> https://cakeml.org/purecake/ <https://cakeml.org/purecake/>
>
> Sent from ProtonMail <https://protonmail.com>, Swiss-based encrypted email.
>
> --
> You received this message because you are subscribed to the Google
> Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to idris-lang+...@googlegroups.com
> <mailto:idris-lang+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/idris-lang/mED8JqG9w5iPgfkXD_SAOW28m2s3XzxWOWI5q7bycFyiq3FTEoy99VbWDd3CyE4kXXvGF3dK7OUlaTSyx-rRi1IYwmnODsrdP7lLuGmV1p4%3D%40protonmail.com <https://groups.google.com/d/msgid/idris-lang/mED8JqG9w5iPgfkXD_SAOW28m2s3XzxWOWI5q7bycFyiq3FTEoy99VbWDd3CyE4kXXvGF3dK7OUlaTSyx-rRi1IYwmnODsrdP7lLuGmV1p4%3D%40protonmail.com?utm_medium=email&utm_source=footer>.

[jonas.cl]

Thanks for the very elaborate answer! I guess that you are right that at this time formal verification for Idris doesn't really make sense. The design space for dependent types are not investigated yet. Haskell-like languages have a long history and that's maybe why they chose to verify a language like that.

Does anyone know about the answers to the other questions regarding rewrite and cumulativity on the Idris todo-list?
Kind regards
Jonas Claesson

Sent from ProtonMail, Swiss-based encrypted email.

> > Sent from ProtonMail https://protonmail.com, Swiss-based encrypted email.

> >
> > --
> > You received this message because you are subscribed to the Google
> > Groups "Idris Programming Language" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> > an email to idris-lang+...@googlegroups.com
> > mailto:idris-lang+...@googlegroups.com.
> > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/idris-lang/mED8JqG9w5iPgfkXD_SAOW28m2s3XzxWOWI5q7bycFyiq3FTEoy99VbWDd3CyE4kXXvGF3dK7OUlaTSyx-rRi1IYwmnODsrdP7lLuGmV1p4%3D%40protonmail.com https://groups.google.com/d/msgid/idris-lang/mED8JqG9w5iPgfkXD_SAOW28m2s3XzxWOWI5q7bycFyiq3FTEoy99VbWDd3CyE4kXXvGF3dK7OUlaTSyx-rRi1IYwmnODsrdP7lLuGmV1p4%3D%40protonmail.com?utm_medium=email&utm_source=footer.
>
>
> --
> You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/eb5e13d1-8be9-41c9-869a-2c614d8f2f63%40tu-dortmund.de.