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…
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):…
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 the goals we…
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…
> 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…
It should be working again within minutes; sorry for the DNS snafu.
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…
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…
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):…
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 the goals we…
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…
> 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…
It should be working again within minutes; sorry for the DNS snafu.
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…