5 ms·
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
by tc 9y ago
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/ 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 https://github.com/rust-lang/rfcs/issues/1930
- throwaway613834 9y agoAren't dependent types undecidable?
- yeahbutbut 9y agoMaybe.
- throwaway613834 9y agoWhat do you mean by "maybe"? [1] https://cs.stackexchange.com/questions/12691 https://cs.stackexchange.com/questions/12691
- yeahbutbut 9y agoI was trying to be punny by implying indecision... edit: also thanks for the link :)
- throwaway613834 9y agoOhh wow that went over my head haha.
- tomp 9y agointegers 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 9y agoDo 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 9y agoGood 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.
- bjz_ 9y agoNo, 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.
- nigeltao 9y agoRe ATS, http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2403.html 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 9y agoATS 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.