Going step by step and making sure the community is OK with what is being hatched is the one and only right approach here, and I applaud the core team for working in that manner.
3 Likes
It’s trivial in dependently-typed languages (it’s their whole point) like Idris, Lean, Agda, etc, where you can operate on types the same way you operate on values, and relatively easy in languages which support some type-level programming like Haskell or PureScript. In all of these, your program simply won’t compile unless your proposition is correct. This of course comes with some trade-offs here and there, but overall if writing highly correct code like this is your goal then these technologies are well-fit for this.
1 Like
It’s also trivial with the SPARK subset of Ada, without having to bring in anything type-related (though you’re of course free to use both).
If you take it far enough you can skip tests altogether because the program is proven to never misbehave, but that’s a wee bit easier to say than to do 
1 Like
Can’t you almost solve this using the same technique you used on your rust example?
Create a Cost type, a Revenue type and a CurrencyHandler module on your system can convert Cost to Integer.
Provided you don’t manually cast Cost|Revenue you only need to test the CurrencyHandler and you have some compiler safety around that logic
I think F# people have a name for something like this, I’m not too familiar with F# so I may be misremembering how some feature works.
Yes you absolutely can, in practice I haven’t seen anyone except Java and C# people doing it (in pretty huge “enterprise” systems). At one point it becomes too unwieldy. Though it could be worth it.
Ultimately you just exchange bugs in your code with bugs in your type specifications.
1 Like
Too much a generalization for my taste but in general you’re not wrong: we’re gonna replace easy-ish correctable programmer bugs with somewhat harder to spot theorem [proving] bugs. 
This is why I am not very fond of the more formal and super strict languages like Coq / Idris / Agda et. al. They sound really good in theory but in practice, most programmers are not mathematicians (though it’s not a bad idea for all of us to be, if you ask me, but we all know it’s not happening en masse for sure).
Languages like Rust and OCaml (likely Haskell as well but I am not familiar with it) are doing just fine and IMO they are striking a golden middle.
1 Like
