Here is an example of a tiny toy compiler proven correct in Idris. It is a small example of the kind of cool things you can do in Dependently Typed languages: h

Here is an example of a tiny toy compiler proven correct in Idris. It is a small example of the kind of cool things you can do in Dependently Typed languages: https://github.com/mbrodersen/idris-sandbox/blob/master/compile-to-stack-machine.idr https://github.com/mbrodersen/idris-sandbox/blob/master/comp...