acfoltzer

3 ms·

1.
by acfoltzer 10y ago
Most people I know who have tried to write large-scale software with annotation techniques have stories that scare me away from ever wanting to experience such. As I mention in another comment, we sometimes describe our goal with Ivory as &
2.
by acfoltzer 10y ago
Thanks for the kind words! You might find our more recent Haskell Symposium paper of interest if you're interested in semantics (this is also a good reminder for us to update the webpage with a link): https://www.cs.indiana.
3.
by acfoltzer 10y ago
Indeed, we're fans of Idris here, and even hosted a series of Idris tech talks: https://galois.com/blog/2015/01/tech-talk-dependently-typed-... The goals of Idris and similar languages are different from
4.
by acfoltzer 10y ago
I'm one of the researchers at Galois who's working on the quadcopter platform for HACMS. Let me first say that this headline makes me cringe just as much as anyone. I'd also like to give folks a pointer to some of the work we
5.
by acfoltzer 12y ago
> I erroneously assumed that it's intended to address implementation errors (that is to replace C or asm implementations with something easier to code). Indeed, and those are absolutely things we need to watch out for when building
6.
by acfoltzer 12y ago
It should be working again within minutes; sorry for the DNS snafu.
7.
by acfoltzer 12y ago
You're dead on. Cryptol is meant first and foremost as an executable specification language. There's an interpreter so that you can run your algorithms on concrete values to make sure that, for example, your test vectors check out