U tweetove putem weba ili aplikacija drugih proizvođača možete dodati podatke o lokaciji, kao što su grad ili točna lokacija. Povijest lokacija tweetova uvijek možete izbrisati. Saznajte više
The hardest thing for programmers learning TLA⁺ is internalising that it is not similar to programming. The goals are different, the scope is different, the language's design requirements and concerns are different, the experience is different, the workflow is different.
Most importantly, the fundamental perspective is different. Programming uses formal text to *construct* a system; in TLA⁺, like in physics, formal text is used to *describe* a system. E.g. https://groups.google.com/forum/#!searchin/tlaplus/balloons%7Csort:date/tlaplus/XsqwpUruTxY/-vz0d51tAQAJ …
Among other things, this means that the very roles of abstraction, composition and encapsulation are drastically different from those they play in programming.
This also sets TLA⁺ apart from similarly-rich logics with proof assistants and/or model checkers that *are* based on programming, like Lean or Agda, and SPIN's Promella or NuSMV's language.
Words being fuzzy and all, I can't parse the difference here. I think of programming as constructing the system by describing it. But maybe TLA+ let's you describe a slice of the system in a way that is not sufficient to construct it?
Yes. Construction requires a deterministic description (or nearly so); if you're describing something with that level of determinism in TLA+ you're either specifying something small at the code level, or are doing it wrong. It doesn't just let you; that's how you *should* do it.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.
