I have a bunch of sketches like this lying around in my home directory, and I'm sure that when I change computers again I will probably forget them. So I'm switching to github for my sketches.
This is a generalization of types, using propositions instead. Not intended as a high-assurance formal verification system, just as a guide like types. But more expressive than representation types.
In informal haskelly-mathematical language I might write something like this:
Definition: i is an index for xs if i is a natural number < length xs.
Definition: If i is an index for xs, then xs !! i is defined by:
(x:xs) !! 0 = x
(x:xs) !! (n+1) = xs !! n
[] !! n contradicts that i is an index for xs
Spec:
index x xs | x `elem` xs = Just i | xs !! i = x
| not (x `elem` xs) = Nothing
By the definition of (!!), the first case of the spec of index implies that i is an index for xs. This is the type signature for index -- a description of its intended behavior. Then I implement it with:
Definition: index x xs is defined by:
index x [] = Nothing
index x (y:ys) | x == y = Just 0
| x /= y = succ <$> index x ys
At this point I would like to be asked to verify that it matches the specification. So my editor would insert:
index x [] = Nothing -- not (x `elem` [])
index x (y:ys) | x == y = Just 0
-- 0 is an index for (y:ys)
-- (y:ys) !! 0 = x
| x /= y = succ <$> index x ys
-- not (x `elem` ys) => not (x `elem` (y:ys))
-- i is an index for ys => succ i is an index for (y:ys)
-- ys !! i = x => (y:ys) !! succ i = x
Some of which could be verified automatically, at which point they would remain silent. The editor tries to verify automatically if it can. Otherwise it leaves the comment in and asks for a line of justification. For example, the first comment in the x /= y case might be difficult to verify automatically, so it would show something like:
-- not (x `elem` ys) => not (x `elem` (y:ys))
--
And you would fill in "since x /= y" -- an explanation intended for humans, not computers. So it does not attempt to provide a formal proof of correctness, but you make the conditions for correctness available to it and it guides you in writing documentation that explains why the code is correct. Further, this documentation is dynamic, so it is aware when an assumption you used changed and possibly invalidated some of your code.
I worry that it would not be aware enough, and ask you to update your reasoning too often. But I don't want to shoot for a fully aware system, since that is the road into proof assistant hell, where it is so much work to verify your work that it's not worth programming anymore. I want to shoot for the same balance Haskell has achieved -- where it makes me think about what I'm doing, but not so much that it stops me when I have a plan. But I am essentially (drastically) extending the newtype concept, of semantic types instead of representation types.
The other thing I'm worried about is that it will not be able to automatically verify enough in real world code and you will be swamped with trivial yet complicated properties to verify. Eg. ys !! i = x => (y:ys) !! succ i = x above: it suffices to show ys !! i = (y:ys) !! succ i, which is more obvious, and yet stronger. How is the computer supposed to know that. Maybe we can do some proof-assistanty things, like allowing you to write "sts" (suffices to show) and then the comment will be replaced with the new thing. When I publish a module, I usually put in a lot of effort into making the source code pretty and well-documented. So such chains would help me do that, not annoy me. Still, it could be a problem if there is too much of it. Maybe that is encouragement to make tight, precise abstractions and limit your assumptions.