[tc]

This DSL seems largely motivated by the desire for provable compile-time bounds checking. One general-purpose modern language that can check bounds at compile time and generate code that is performance-competitive with C is ATS:

http://www.ats-lang.org/

Dependent types are meant to solve exactly this class of problem. Rust has an RFC for adding these:

https://github.com/rust-lang/rfcs/issues/1930

[nigeltao]

Re ATS, http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/... says that "By default, the constraint-solver implemented for ATS/Postiats makes use of the standard arithmetic of infinite precision. For the sake of efficiency, one may also choose to use machine-level arithmetic for solving integer constraints. Due to potential arithmetic overflow, results returned by the constraint-solver that uses machine-level arithmetic can be incorrect".

Puffs does not use infinite precision integers (aka "big ints"), for performance. But Puffs still checks for arithmetic overflow.

Re dependent types, I made a comment elsewhere on this page that "dependent types are one way to prove bounds safety, but they're not the only way".

[doublec]

ATS uses infinite precision ints only for the proof/dependent type checking. The ints used at runtime are machine ints. It's to avoid overflow during type system checking.

[throwaway613834]

Aren't dependent types undecidable?

[bjz_]

No, not if your language has totality checking like Idris, Agda, Lean, etc. Granted, it can sometimes be finicky to prove totality - the type checker naturally has to be a little conservative due to the impossibility of solving the halting problem, but for most things with array bounds checking it shouldn't be an issue.

[tomp]

integers with additions are decidable - that's pretty much what you need to verify array bounds (multiplication with a constant is included as well, so matrices should work too).

[throwaway613834]

Do you mean "in practice" that's what you need? I could buy that, but I'm thinking about it in terms of the language spec. What would it say? Are we moving toward a language spec that says the meaning is "whatever the reference compiler can handle"? Or do you mean one that says "array indices may only be (constant) linear combinations of variables in order for the code to be compilable" or something like that?

[tomp]

Good point. The way I imagined is, the language is defined as "safe", and has both "static" and "dynamic" guarantees. Whatever the compiler is able to prove statically, amazing, or else it adds dynamic checks. The programmer can optionally tag the function/expression so that the compiler will warn if it can't prove it. Long-term, I think it's very reasonable to assume the solvers will improve, so best to design a language with this in mind.

[yeahbutbut]

Maybe.

[throwaway613834]

What do you mean by "maybe"?

[1] https://cs.stackexchange.com/questions/12691

[yeahbutbut]

I was trying to be punny by implying indecision...

edit: also thanks for the link :)

[throwaway613834]

Ohh wow that went over my head haha.