Re:Concepts: The Future of Generic Programming [pdf]
by wyager on Tuesday December 20, 2016 @10:27PM
(#13226590)
You can do this with coq/agda/idris (fully general dependent types) or Haskell (LiquidHaskell). Not C++.
LiquidHaskell is nice because it's all written in comments next to or in a separate file from your Haskell code. This means the Haskell compiler doesn't even have to know about it. On the other hand, when you're using something like Idris for formal programming, you often find your program full of proof witnesses that you aren't actually using for your real code you want to write. You can prove all sorts of things, like that a function only returns negative multiples of 3, or only returns vectors of length 5n+1.
LiquidHaskell is nice because it's all written in comments next to or in a separate file from your Haskell code. This means the Haskell compiler doesn't even have to know about it. On the other hand, when you're using something like Idris for formal programming, you often find your program full of proof witnesses that you aren't actually using for your real code you want to write. You can prove all sorts of things, like that a function only returns negative multiples of 3, or only returns vectors of length 5n+1.