1. 43

  2. 1

    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.

    1. 5

      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.

      1. 1

        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.