We need a model that lets us assimilate gradual improvements in automatic reasoning, like better SMT solvers, without requiring us to re-type (pun intentional) our code.
Are efforts to integrate SMT solvers into ML or other programming languages. That sounds interesting but also hard to imagine.
There are a few efforts. The one I know best is Liquid Haskell which adds extra typing information in comments refining the basic Haskell types with SMT-checkable predicates.
Interesting article.
We need a model that lets us assimilate gradual improvements in automatic reasoning, like better SMT solvers, without requiring us to re-type (pun intentional) our code.
Are efforts to integrate SMT solvers into ML or other programming languages. That sounds interesting but also hard to imagine.
There are a few efforts. The one I know best is Liquid Haskell which adds extra typing information in comments refining the basic Haskell types with SMT-checkable predicates.
It’s a bit more common than you might think, e.g. gcc has several solvers in its optimization path.
There are also programming languages which explicitly target solvers, like SMT-LIB.