5 ms·

Interesting. How do you reconcile this: "Julia's type system is designed for semantics specification, not proofs, so it's not really what you'd want to use the

Interesting. How do you reconcile this: "Julia's type system is designed for semantics specification, not proofs, so it's not really what you'd want to use there." With "think the most promising way to go is basically to let the users specify their own correctness criteria (for example, some people really care about correctness of array dimensions), and then just go to a full theorem proving system"

KenoFischer 6y ago
Oh, you just don't do correctness proofs over the same type system that is used for dispatch (i.e. "the Julia type system"). We already use an expanded lattice internally for reasoning about Julia code, so there's really no problem just doing something completely general.
- dklend122 6y ago
  So you make the type lattice user extendable? Or different layers hardcoded? If the former, how do you get code reuse? What do you mean by expanded lattice? I thought the type lattice was fixed. What would something general look like ? Thanks for humoring my naive question(s).
  - oxinabox 6y ago
    I am guessing it is the thing where if you look at `@code_typed` you will see sometimes annotated not just with types but with `Const(42)` which shows where constant folding is occuring
  - gugagore 6y ago
    This post discussion might help: https://discourse.julialang.org/t/julia-inference-lattice-vs-type-lattice-from-the-tpu-paper/18397/2 https://discourse.julialang.org/t/julia-inference-lattice-vs... As far as I know, currently the non-julia-types type lattice is hardcoded. But even if that's the case, that's not fundamental to the design. > If [you make the type lattice user extendable], how do you get code reuse? What kind of code reuse do you mean? This alternative type lattice is not supposed to change the semantics of any Julia program, aside from rejecting programs that would otherwise have semantics in Julia.

KenoFischer 6y ago

Oh, you just don't do correctness proofs over the same type system that is used for dispatch (i.e. "the Julia type system"). We already use an expanded lattice internally for reasoning about Julia code, so there's really no problem just doing something completely general.

dklend122 6y ago
So you make the type lattice user extendable? Or different layers hardcoded? If the former, how do you get code reuse? What do you mean by expanded lattice? I thought the type lattice was fixed. What would something general look like ? Thanks for humoring my naive question(s).
- oxinabox 6y ago
  I am guessing it is the thing where if you look at `@code_typed` you will see sometimes annotated not just with types but with `Const(42)` which shows where constant folding is occuring
- gugagore 6y ago
  This post discussion might help: https://discourse.julialang.org/t/julia-inference-lattice-vs-type-lattice-from-the-tpu-paper/18397/2 https://discourse.julialang.org/t/julia-inference-lattice-vs... As far as I know, currently the non-julia-types type lattice is hardcoded. But even if that's the case, that's not fundamental to the design. > If [you make the type lattice user extendable], how do you get code reuse? What kind of code reuse do you mean? This alternative type lattice is not supposed to change the semantics of any Julia program, aside from rejecting programs that would otherwise have semantics in Julia.