3 ms·
> Do you have an example of a language that does what you're looking for? Dependently typed programming languages such as Coq and Idris let you write proofs ab
by curryhoward 9y ago
> Do you have an example of a language that does what you're looking for?
Dependently typed programming languages such as Coq and Idris let you write proofs about your programs. These languages are fairly academic, and most engineers probably won't find it worthwhile to use these tools. Personally, I love them. I wrote a short article about my experience with Coq: https://www.stephanboyer.com/post/134/my-unusual-hobby https://www.stephanboyer.com/post/134/my-unusual-hobby
- lmm 9y agoRust has the same level of rigour, other than lacking totality. Not having dependent types makes properties a lot more cumbersome and less practical to encode, but the actual proofs you get of the properties you do model are just as valid as those in Coq and Idris (modulo nontermination).