[_flux]

Personally I would enjoy if TLA+ would have types, though, and TLA+ belongs to the land of logic, right? I do not know how it differs from the abstraction logic referred in your writing and your other whitepapers.

What is commonly used is a TypeOK predicate that verifies that your variables have the expected type. This is fine, except your intermediate values can still end up being of mis-intended values, so you won't spot the mistake until you evaluate the TypeOK predicate, and not at all if the checker doesn't visit the right corners of the state space. At least TypeOK can be much more expressive than any type system.

There is a new project in the same domain called Quint, it has types.

[practal]

Practically, in abstraction logic (AL) I would solve that (AL is not a practical thing yet, unlike TLA+, I need libraries and tools for it) by having an error value ⊥, and making sure that abstractions return ⊥ whenever ⊥ is an argument of the abstraction, or when the return value is otherwise not well-defined [1]. For example,

    div 7 0 = ⊥, 

and

    plus 3 ⊥ = ⊥, 

so

    plus 3 (div 7 0) = ⊥.

In principle, that could be done in TLA+ as well, I would guess. So you would have to prove a predicate Defined, where Defined x just means x ≠ ⊥.

[1] Actually, it is probably rather the other way around: Make sure that if your expression e is well-defined under certain preconditions, that you can then prove e ≠ ⊥ under the same preconditions.

[thechao]

This looks like you've defined the abstract lattice extension as a proper superset of the concrete semantics. That sort of analysis is entirely subsumed by Cousot & Cousot's work, right? Abstract Interpretation doesn't require static types; in fact, the imposition of a two-level interpretation is secondary. The constraints on the pre-level are so that the behavior of the program can be checked "about as quickly as parsing", while also giving strong correctness guarantees under the systems being checked.

Moving the whole thing to dynamic behavior doesn't tell us anything new, does it? Lisps have been tagged & checked for decades?

[practal]

I have not defined any "abstract lattice extension" explicitly; which is nice, why would I need to know about lattices for something as simple as this? It is just a convention I suggest to get a useful Defined predicate, actually. Nobody can stop you from defining mul 0 ⊥ = 0, for example, and that might make sense sometimes.

I would suggest that abstraction logic compares to type theory as Lisp compares to Standard ML; but that is just an analogy and not precise.

[thechao]

My problem with your interaction on this forum, so far, is that it kind of ignores the practical (artisan) craft of programming. The use of static type systems by working engineers isn't math; it's more akin to "fast, formal checking". You can assert that you don't like types, or they're useless all day long; but, every working engineer knows you're wrong: static type systems have solved a real problem. Your arguments need to be rooted in the basic experience of a working engineer. Single-level programming has its place, but runtime checking is too error prone in reality to build large software. If you think this isn't true, then you need to show up to the table with large scale untyped software. For instance: the FORTH community has real advantages they've demonstrated. Where's your OS? Your database? Your browser? If you have real advantages then you'd have these things in hand, already.

Otherwise, you're just another academic blowhard using a thin veneer of formalism to justify your own motivated reasoning.

[practal]

Strong opinion! Also, it seems you didn't read my interaction so far carefully enough. You also didn't read the summary I linked to, otherwise you would know that I fully approve the current use of types in programming languages, as they provide lightweight formal methods (another name for what you call "fast, formal checking"). But I think we will be able to do much better, we will have fast, formal checking without static types. Not today, not tomorrow, but certainly not more than 10 years from here.

[thechao]

I'm reading through your paper, and I really like your ideas. I just think you're approaching the engineers wrong.

[deredede]

> At least TypeOK can be much more expressive than any type system.

Can you clarify what you mean by that? Dependent types or more practically refinement types (à la F*) can embed arbitrary predicates.

[_flux]

Right, I was referring totype systems in relatively popular real-world programming languages of today, i.e. Haskell, OCaml, Rust, Haskell :).