3 ms·
Glad to hear you say that. Aside from that the work seems very interesting. I am going to check out Ivory. I have been reading up and playing with Idris and F.
by eggy 10y ago
Glad to hear you say that.
Aside from that the work seems very interesting. I am going to check out Ivory. I have been reading up and playing with Idris and F.
I like F so far, and that you can output F# and OCaml. Idris's goals seem in line with what you were originally looking for. Have you evaluated it?
- eggy 10y ago[Edit] Replying to my post to edit, since no choice given to edit. Should say "I like Fstar" above, but asterisk turned on italics...
- acfoltzer 10y agoIndeed, 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-functional-programming-idris-1-3/ https://galois.com/blog/2015/01/tech-talk-dependently-typed-... The goals of Idris and similar languages are different from the goals we had with Ivory, though. We sometimes describe Ivory as "medium-assurance" as opposed to the high assurance one can get from a language with a more expressive type system. It makes sense for some systems or components to be formally verified, for example the seL4 verified microkernel which is also used on our copter. However we simply would not have been able to formally verify (or even get to typecheck with fancier dependent types) something on the scale of an autopilot given the resources we had on the project. Instead we rely on getting quite a bit of bang for the buck with the memory safety features, and then augment with assertions. We ended up with a working autopilot (and board-support package with drivers) in only ~4 engineer-years, so we think the tradeoff is working well so far :)
- eggy 10y agoSounds great. I'll check out the talks link and Ivory some more. Thanks!