4 ms·
We already have a basic form of machine checked-proofs in everyday code: type systems. Type systems encode and prove simple theorems like "f(x: int) -> int ret
by jpochtar 9y ago
We already have a basic form of machine checked-proofs in everyday code: type systems. Type systems encode and prove simple theorems like "f(x: int) -> int returns an int, if x is an int". Typescript and Mypy show us that these proof checkers don't need to be built into a language. Even better, they show that proofs can be over subsystems of a program, since Typescript and Mypy both allow for partial/incremental typing. We just need to extend these systems to support more complex theorems.
- earleybird 9y agoand you end up in the neighbourhood of Idris which is, I find, a pleasant experience when doing development
- bcherny 9y agoIncremental type systems are super interesting. Lots of work being done in the last 10 years that blurs the lines between static and dynamic typing (monkeytype, reticulated Python), types and values (via the triumph of inferred types), kinds and types (powerful trait systems like Scala's), and even values and code (code synthesis like magichaskeller, or excel's flashfill). A bit of self promotion, I touched on this in a recent blog post if you're interested in this sort of stuff: https://performancejs.com/post/hde6a33/JavaScript-in-2017:-Year-in-Review,-Predictions-for-2018 https://performancejs.com/post/hde6a33/JavaScript-in-2017:-Y...