Will Idris let you do "low level" programming (like ATS) one day?

[Max Hayden Chiz]

I'm new to Idris and only recently learned it from the _Type Driven Development_ book. But I was impressed with what I saw.

Obviously it's still got a lot of rough edges, but I really like what's there now, *especially* the usability and ergonomics. I'm probably biased based on my background -- FinTech, where a code error in some loop that runs every few miliseconds could cost you millions, and before that active safety automotive systems where code errors kill people. But what I personally like about Idris is the potential to let me do my job in *one* language *with* high assurance throughout. Right now I work in a combination of (mostly) OCaml, (a little) C/C++, and (experimentally) a bit of Rust. But OCaml is limited in what it can prove on its own and even Rust has to have "unsafe" mode. (And OCaml's run-time, rather obnoxiously, isn't thread safe despite a good design for this having been around for some time now. https://github.com/ocamllabs/ocaml-multicore)

At least in principle Idris would let me do *all* of my development in a provably safe way from one language because you could, in some future version of the language, do all of the "unsafe" low-level C/Rust stuff safely.

In theory, ATS lets you do this now. (If you aren't familiar with ATS see https://www.youtube.com/watch?v=zt0OQb1DBko or even if you are, the talk is entertaining and humorous.) However, despite letting you write provably safe "C" code, ATS has basically no usability or programmer ergonomics. I like the *idea*, but it isn't (currently) a usable OCaml replacement for higher level code, and the code-bloat over C for low-level stuff is close to 50%. It would be great if Idris could one day do a better of job of this. (In particular ATS code can be *exactly* as performant as C code, and that's a hard requirement for that low-level stuff because it's often real-time in nature.)

Another problem with ATS is that converting C code to safe code is painful. If Idris made the "convert from C" thing sufficiently easy, you might even see some uptake among C-based open source projects with a security or reliability bent. The problem is that no one will rewrite a multi-million line code-base from C to Idris, but if there was a convenient way to "convert" at least most C code over and then gradually start taking advantage of the typing system, the uptake would probably be more extensive. "Convert you C code and get verification for free" would be a killer app for lots of people. I *think* it's probably doable. The CCured application could prove that around 90% of C was safe, another 9% was unsafe just because it couldn't prove bounds checks (which the dependent typing can handle), and so that leaves 1% that needs to be manually fixed, and even there some of that could be automated. (It also didn't handle resource leaks, but you can deal with that in Idris in several conceivable ways.)

Even if an app that auto-converts C code isn't doable, I think one of the key advantages of dependent types is that they let you do the "dangerous" stuff safely. (And that advantage is kind of lost if you focus on making a good web-framework.) So I'm hoping that one day Idris will be at the point where I can (hopefully gradually) use it instead of OCaml/C.

So is this something that Idris plans to be usable for one day? Or is the goal more to focus on allowing for the design of safe low-level DSLs instead of ATS's full-on C replacement?

Thanks again for a great language. I'm looking forward to seeing where it goes.

--Max Chiz

New Orleans, LA

[Alexander Gryzlov]

It'd probably be easier to first define a safe EDSL and then provide a source-to-source transpiler into it from C. I guess a mid-tier goal would be to have an equivalent of https://ivorylang.org/ or http://feldspar.github.io/ in Idris.

Of course there's a lot of missing building blocks involved, a basic one for example is treatment of fixed-size binary numbers. I've made a rough translation of verified binary modular arithmetics from Coq at https://github.com/sbp/idris-bi/tree/master/src/Data (see BizMod2), but it definitely needs some automation a-la presburger/ring solver, and the type checker is, let's say, not too fast when checking such proofs. Another part of that puzzle missing is a bitvector representation, which would be easier to reason about for purely logical operations like shifts/rolls. Some volunteer might want to port something like https://github.com/maximedenes/coq-amd64/blob/master/src/bitsrep.v ;)

One could also reuse existing tools like SMT solvers to offload parts of typechecking. The problem with that is that AFAIK elaborator reflection (basically Idris' "macro" facility) currently doesn't allow running arbitrary IO code after typechecking has started.

Also, I should mention there's some very raw support for linear types in Idris, which also might potentially help a lot with imperative-style programming.

Alex

[David Thrane Christiansen]

On 20-01-2018 13:24, Alexander Gryzlov wrote:
> One could also reuse existing tools like SMT solvers to offload parts of
> typechecking. The problem with that is that AFAIK elaborator reflection
> (basically Idris' "macro" facility) currently doesn't allow running
> arbitrary IO code after typechecking has started.

You're right that elaborator reflection doesn't allow IO, but it is
possible to use a top-level type provider that executes between two
elaborator reflection steps.

A sketch could be:

1. Run an Elab action that leaves behind a type declaration with a
particular name as well as a string that contains the input to the SMT
solver

2. Use a type provider to call out to an SMT solver with the string as
input to check some proposition and postulate something appropriate

3. Run another Elab action that fulfills the original obligation with
the postulate

It's a bit hairy, but I've done similar things before at a smaller scale.

/David