That's cool (Idris seems to have an infinitely pluggable back end), but it's not the same thing. You can code in a higher-level language, but you can't inspect

That's cool (Idris seems to have an infinitely pluggable back end), but it's not the same thing. You can code in a higher-level language, but you can't inspect another program's guarantees and you can't safely use them within your own system.