4 ms·

I'd personally like to find the time to write this – some of the infrastructure (like call graph analysis) is already available. However, I think this is the n

by llogiq 11y ago

I'd personally like to find the time to write this – some of the infrastructure (like call graph analysis) is already available. However, I think this is the nuclear option. I have some experience from university where I wrote some Eiffel code, contracts and all that jazz. It often takes some head scratching to figure out the right pre- and postconditions. I'd actually rather see more safe interfaces for the common cases (like iterators and slices) that are ergonomic to use and may actually carry the proof in their types.

catnaroek 11y ago
Eiffel contracts are still checked at runtime, which kind of defeats the point - the real payoff of enforcing an invariant statically is not having to check it dynamically! What I'm talking about is using a special kind of theorem prover called “SMT solver” to guarantee at compile time that your array indices are always valid, eliminating the need to perform bounds checking at runtime. In many cases, SMT solvers require little to no programmer-supplied annotations, which makes them more ergonomic than full-blown dependently typed programming languages like Coq, Agda, Idris, etc.
- llogiq 11y ago
  There are tools to do exactly that (I don't remember the name of what we used at university, alas). And no, I do not want to run a SMT solver against anything but simple code, because my build is slow enough as is. ;-)
  - catnaroek 11y ago
    Most index manipulation is fairly simple. For instance, if the result of `str.find(pat)` is `Some(pos)`, then you know that: (0) `pos <= str.len()`. (1) `pos` is actually the beginning of a character - it makes sense to split the string at the position `pos`. These things are easy to check - there is not even any multiplication involved! - but a conventional type checker won't do. Much of the pain of using dependent types is the result of sticking to unification as the only basis for type-checking.
    - llogiq 11y ago
      On the contrary, it's actually rather easy to use the type checker to encode this: Just make a wrapper type CharIdx(usize) that encodes the fact that the enclosed value is a valid char position and implement Index for it using unchecked indexing. Also implement Index for usize with the usual check for bounds and valid character position.

by llogiq 11y ago

catnaroek 11y ago

Eiffel contracts are still checked at runtime, which kind of defeats the point - the real payoff of enforcing an invariant statically is not having to check it dynamically! What I'm talking about is using a special kind of theorem prover called “SMT solver” to guarantee at compile time that your array indices are always valid, eliminating the need to perform bounds checking at runtime. In many cases, SMT solvers require little to no programmer-supplied annotations, which makes them more ergonomic than full-blown dependently typed programming languages like Coq, Agda, Idris, etc.

llogiq 11y ago
There are tools to do exactly that (I don't remember the name of what we used at university, alas). And no, I do not want to run a SMT solver against anything but simple code, because my build is slow enough as is. ;-)
- catnaroek 11y ago
  Most index manipulation is fairly simple. For instance, if the result of `str.find(pat)` is `Some(pos)`, then you know that: (0) `pos <= str.len()`. (1) `pos` is actually the beginning of a character - it makes sense to split the string at the position `pos`. These things are easy to check - there is not even any multiplication involved! - but a conventional type checker won't do. Much of the pain of using dependent types is the result of sticking to unification as the only basis for type-checking.
  - llogiq 11y ago
    On the contrary, it's actually rather easy to use the type checker to encode this: Just make a wrapper type CharIdx(usize) that encodes the fact that the enclosed value is a valid char position and implement Index for it using unchecked indexing. Also implement Index for usize with the usual check for bounds and valid character position.