321–330 of 448 posts
Earlier quoted context omitted.
Through empirical evidence? Do you think that the vast majority of software devs moved to typing for no reason?
We don't actually have empirical evidence on the topic, surprisingly. It's just people's hunches.
I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…
A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in…
That is not novel and every declarative language precisely embodies it.
Earlier quoted context omitted.
> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many…
Can TLA+ prove anything about something you specify but don't execute?
- TLAPS is the interactive proof system that can automate some proof steps by delegating to SMT solvers: https://proofs.tlapl.us/doc/web/content/Home.html
- Apalache is the symbolic model checker that delegates verification to Z3. It can prove properties without executing anything, or rather, executing specs symbolically. For instance, it can do proofs via inductive invariants but only for bounded data structures and unbounded integers. https://apalache-mc.org/
- Finally, TLC is an enumerative model checker and simulator. It simply produces states and enumerates them. So it terminates only if the specification produces a finite number of states. It may sound like executing your specification, but it is a bit smarter, e.g., when checking invariants it will never visit the same state twice. This gives TLC the ability to reason about infinite executions. Confusingly, TLC does not have its own page, as it was the first working tool for TLA+. Many people believe that TLA+ is TLC: https://github.com/tlaplus/tlaplus
Earlier quoted context omitted.
A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in…
> No one claims that good type systems prevent buggy software. That's exactly what languages with advanced type systems claim. To be more precise, they claim to eliminate entire classes of bugs. So they reduce bugs, they don't eliminate them completely.
Earlier quoted context omitted.
TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Us…
> You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” You really don't. It's not LTL. Abstraction/refinement relations are at the core of TLA. > Or even floats [0] and it becomes challenging and strings are a mess. No problem with floats or strings as far as specification goes. The particular verification tools you choose to run…
You are talking about the logic of TLA+, that is, its mathematical definition. No tool for TLA+ can handle all of mathematics at the moment. The language was designed for specifying systems, not all of mathematics.
I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…
Earlier quoted context omitted.
And one can see how quickly they became mainstream...
I think that’s because the barrier to entry for a beginner is much higher than say python.
Earlier quoted context omitted.
> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many…
TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Us…
I think people get confused by the word "temporal" in the name of TLA+. Yes, it has temporal operators. If you throw them away, TLA+ (minus the temporal operators) would be still extremely useful for specifying the behavior of concurrent and distributed systems. I have been using TLA+ for writing specifications of distributed algorithms (e.g., distributed consensus) and checking them for about 6 years now. The question of liveness comes the last, and even then, the standard temporal logics are barely suitable for expressing liveness under partial synchrony. The value of temporal properties in TLA+ is overrated.
Earlier quoted context omitted.
I think that’s because the barrier to entry for a beginner is much higher than say python.
IMHO, these strong type systems are just not worth it for most tasks. As an example, I currently mostly write GUI applications for mobile and desktop as a solo dev. 90% of my time is spent on figuring out API calls and arranging layouts. Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive. Even at the backend a…
this is exactly where a good type system helps: you have an unvalidated string and a validated string which you make incompatible at the type level, thus eliminating a whole class of possible mistakes. same with object ids, etc.
don't need haskell for this, either: https://brightinventions.pl/blog/branding-flavoring/
Earlier quoted context omitted.
> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code. However, even…
> but one reaps the benefits later thanks to more confidence when refactoring or adding code. To be honest, I believe it makes refactoring/maintenance take longer. Sure, safer, but this is not a one-time only price. E.g. you decide to optimize this part of the code and only return a reference or change the lifetime - this is an API-breaking change and you have to potentially recursively fix it. Meanwhile GC languages…