Just to note, Edwin was the original author of Idris, so I'd definitely recommend watching his talk. Edit: Given that my comment seems fairly high at the mome

Just to note, Edwin was the original author of Idris, so I'd definitely recommend watching his talk. Edit: Given that my comment seems fairly high at the moment, I'll post a link to his PhD thesis, which seems to be the genesis of Idris for anyone interested: http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf