Very interesting case study on using a type-safe language to produce driver code in constrained embedded systems.
The Ajhc compiler mentioned in the paper has a page at http://ajhc.metasepi.org/ – the first thing it says is that the research group which developed it has switched to ATS.
There’s been a few submissions on that here already:
I thought Haskellers or people with other safe languages might find this one interesting. Low-level work in Haskell might also payoff if and when Habit language gets revived. Im kind of surprised it even paused given Galois probably has enough use for that to build a prototype themselves.
From http://www.metasepi.org/en/posts/2015-12-31-yuku-kuru.html it
looks like the author spent all of 2015 learning ATS but didn’t have much to show at the end.
Regarding Habit, I guess we’ll see: https://galois.com/blog/2017/12/update-habit-programming-language/
That update is what I was talking about. Far as ATS, I keep seeing people on forums call it and Idris “practical” languages. Yet, Ive seen many smart folks quit when trying to learn them. I doubt they’re really practical yet given even SPARK with its automation is still work.
Author would probably be better off continuing to stretch Haskell. Ive also seen one or two people alk of mixing it and Rust for the latter preserving some of its high-level features and safety with extra efficiency. Perhaps implementing anything low-level in Haskell in Rust or even ATS would be a neat project.
I think Idris is an intersting case: the developers have very fresh thoughts about the practice of programming. This can be seen in their attempt to provide an interactive programming experience through typed holes, a language server and a very lenient parser that tries to figure out as much as it can. I once saw Brady speak about Idris and he mostly talked about how programs are broken syntactically and logically during development most of the time. That was very intersting.
Also, Idris aims to be a practical programming language, but not an industry language. It intends to be a research language and owns that. It becomes very apparent from their 1.0 post: https://www.idris-lang.org/idris-1-0-released/
Key part of your link:
“which aims to make theorem proving and software verification accessible and practical for software developers in general”
What your describe is interesting. I like that they’re researching those things. Their definition of practical, though, is that regular software developers will be able to use it. The ones I know that tried both ATS and Idris gave up on it as too difficult to do even basic stuff. A few saying regular developers shouldn’t use it had experience with lightweight formal methods like model-checkers that do benefit regular developers. The people doing big time formal methods are still in a debate about how useful such a language is for research. What most of them said was to just learn Coq, Isabelle/HOL, etc. Especially since most work in formal verification use those with a resulting ecosystem building up of both prototyped ideas and implementations.
I only know three, code-level, formal approaches that general developers were successful with when they made attempts: Mill’s Cleanroom, Meyer’s Design-by-Contract, and SPARK Ada. I hope Idris joins the ranks. Who knows, it might be a lot easier to learn and use for practical components today than it was as recently as a year ago when I was reading negative information. Unless it has, I just don’t think calling it practical makes sense unless qualified with “for use by highly-skilled people who could’ve already done the project in Coq.” Suddenly, the mental image of the Idris market goes from huge to tiny.
Now, on the side, I would find it interesting to know how many people who got used to Rust managed to learn Idris. Folks who also weren’t of strong, math background or something. Just programmers willing to learn. The reason being the borrow-checker is a lot like a lightweight, formal method the person learns through lots of trial and error until developing an intuition for how to structure his or her problems correctly. Those who were able to do that might also learn to do the same with Idris either fully or up to some subset of its capability. If fully, that’s extra corroboration for Idris’s design. If a subset, that tells us where some low-hanging fruit is in dependently-typed programming.