I’d heard of Idris. Parts of it sound really good (dependent typing, totality, a proper effects system, being usable from Vim), although I’m not a huge fan of tactic-based proofs (that’s what the Curry-Howard Isomorphism is for!). It’s definitely on the top of my list of languages to learn. I wasn’t aware of the security focus, that is certainly interesting.
Proving safety in the face of malicious input sounds fascinating—a dump would be much appreciated.
I have not actually learned Idris yet, and I think I could motivate myself better if I had a study partner; would you be interested in something like that?
Depends mainly on how we both learn best. For me, when it comes to learning a new language that tends to be finding a well-defined, small (but larger than toy) project and implementing it, and having someone to rubber-duck with (over IM/IRC/email is fine) when I hit conceptual walls. I’m certainly up for tackling something that would help out MIRI.
Also, presuming that the talk Andreas Bogk has proposed for 30c3 is accepted, you’ll want to see it—it’s a huge pragmatic leap forward. (I apologize for not being at liberty to go into any more detail than that. The talk will be livestreamed and recorded, FWIW.)
I’d heard of Idris. Parts of it sound really good (dependent typing, totality, a proper effects system, being usable from Vim), although I’m not a huge fan of tactic-based proofs (that’s what the Curry-Howard Isomorphism is for!). It’s definitely on the top of my list of languages to learn. I wasn’t aware of the security focus, that is certainly interesting.
Proving safety in the face of malicious input sounds fascinating—a dump would be much appreciated.
“Security Applications of Formal Language Theory” is a good overview. (If you don’t have IEEE access, there’s a tech report version.) Much of the work going on in this area has to do with characterizing classes of vulnerabilities in terms of unintended computational automata that arise from the composition of independent systems, often through novel vulnerability discovery motivated by considering the formal characteristics of a composed system and figuring out what can be wedged into the cracks. There’s also been some interesting defensive work (Haskell implementation, an approach I’m interested in generalizing). That’s probably a good start.
I have not actually learned Idris yet, and I think I could motivate myself better if I had a study partner; would you be interested in something like that?
I might be interested in being your study partner; what would that involve?
Depends mainly on how we both learn best. For me, when it comes to learning a new language that tends to be finding a well-defined, small (but larger than toy) project and implementing it, and having someone to rubber-duck with (over IM/IRC/email is fine) when I hit conceptual walls. I’m certainly up for tackling something that would help out MIRI.
Sounds like fun! I’ll PM you my contact details.
What do you mean by having a study partner?
Also, presuming that the talk Andreas Bogk has proposed for 30c3 is accepted, you’ll want to see it—it’s a huge pragmatic leap forward. (I apologize for not being at liberty to go into any more detail than that. The talk will be livestreamed and recorded, FWIW.)