3 ms·
In a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.
by groar 11y ago
In a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.
- mafribe 11y agoSure, but as of July 2015 the programming languages (e.g. Agda, Idris) that can give full specifications of their own programms, are experimental, not mainstream.
- black_knight 11y ago«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple things are rather difficult. But I think this will improve as we learn the right way to look at things.