I like Alloy, especially after they added the new temporal features in version 6.
Last time I played with it, it had to be used from inside some awful IDE though. I know this is a common complaint, my point is not to repeat it. What I wanted to say is that while I was browsing the download page for Alloy just now, I noticed that it links to Sterling: A Web-based Visualizer for Relational Modeling Languages. I was hoping it would allow me to use my own editor and do custom visualisations in a browser, this doesn’t seem to be the case, rather it’s a new web-based IDE.
However, as I was skimming through the Sterling paper, I noticed that it said that Sterling also “is the visualizer for an Alloy-like model finder called Forge, which is being developed at Brown University and is used to teach a Logic for Systems class of over 60 students”. So I looked up Forge, it appears to be a Racket “language”/eDSL which looks like Alloy. I’m still not sure what the exact difference is, their readme says “Forge is heavily adapted from the excellent Alloy, a more widely used and somewhat more scalable tool. Forge and Alloy even use the same engines!”, but also “For broader historical context on Forge, the Alloy documentation or an Alloy demo may be useful. We don’t suggest using these as reference for Forge itself, however.”. In either case, it seems Forge might be a way to get a taste of Alloy without the sour taste of their IDE!
Hi, I’m one of the authors of Alloy 6 and of this new book.
I think the image of the Alloy Analyzer your depicting is a bit too dark. The IDE is quite sophisticated since it features an interconnection of a solving engine, a rich visualizer as well as a very useful evaluator (to navigate instances and counterexamples). Compared with other formal methods, I think Alloy is quite good in terms of user-friendliness and usefulness of results it provides. The legacy integrated editor is on the other hand quite basic but, considering models in Alloy are rather small, the -real- annoyances remain limited in my view (the editor has syntax highlighting, error reporting, find&replace…). An interesting aspect for non-power users is that this is all delivered in a single, ready-to-run JAR file. This is in particular invaluable with students (Alloy is taught in several universities, at least in Europe and in America).
A future version will allow users to rely on LSP and use an editor of their choice (there were already some experiments with LSP and there actually is an unofficial VSCode plugin but it’s not up to date). As an “epxert” user myself, what I would not want, however, would be to lose the the above-mentioned sophisticated interactions present in the tool, for the sake of getting a slicker editing experience.
Alloy 6.2 now has a command line but it’s not that great for solving, more for automated build chains. Many serious Alloy users I know use the Vscode extension.
The new A6.2 command line indeed allows to execute the same kinds commands than in the GUI, with roughly the same options, so it’s mainly aimed at facilitating batch verification and benchmarks, I’d say.
For people who do not know the Alloy Analyzer completely, this is different from the Evaluator feature mentioned above, which allows to query, in Alloy itself, an instance or counter-example currently being shown by the Visualizer. This feature, which isn’t new by the way, is very useful in practice when models become complex.
Finally, the VSCode extension does not use Alloy analyzer 6.1 nor 6.2 but it ships a tailored version, AFAIK. It’s indeed already great but, hopefully, in the future, we will be able to get a plugin that can connect to the “real”, official Alloy.
The main thing refraining me to use tools other than pdflatex+bibtex is that they don’t seem to be compatible with the requirements of scientific editors. How do other scientists address this?
Typst has a proven track record of being able to imitate the style of various scientific journals. It seems reasonable to bet that even if your particular template is not currently supported, someone could port it. So you could either wait for someone else to do it, or try doing it yourself.
I would be curious to give Typst a try, and my idea is to start with some area where style requirements are less stringent: grant proposals for example, but actually I would like to try it for slides. I find beamer unpleasantly heavy to use. I often prototype my slides in Markdown first, and I think that Typst could remove this intermediate step and provide a pleasant experience thanks to live rendering. (Re. live rendering: texpresso provides live rendering for LaTeX, and it does improve things noticeably for beamer slides.)
That said, some tools expect LaTeX sources as part of their pipeline – arXiv for example expects “sources” and it means LaTeX, and they built a lot of custom tooling to work with the TeX sources. I don’t think they will be usable with Typst for a long while, except maybe if people were to find a way to write a good-enough translator from Typst to LaTeX.
Typst has a proven track record of being able to imitate the style of various scientific journals. It seems reasonable to bet that even if your particular template is not currently supported, someone could port it. So you could either wait for someone else to do it, or try doing it yourself.
I would be curious to give Typst a try, and my idea is to start with some area where style requirements are less stringent: grant proposals for example, but actually I would like to try it for slides. I find beamer unpleasantly heavy to use. I often prototype my slides in Markdown first, and I think that Typst could remove this intermediate step and provide a pleasant experience thanks to live rendering. (Re. live rendering: texpresso provides live rendering for LaTeX, and it does improve things noticeably for beamer slides.)
That said, some tools expect LaTeX sources as part of their pipeline – arXiv for example expects “sources” and it means LaTeX, and they built a lot of custom tooling to work with the TeX sources. I don’t think they will be usable with Typst for a long while, except maybe if people were to find a way to write a good-enough translator from Typst to LaTeX.
Last time I tried to use TLA+ I got very much repulsed by how hacky and amateurish it felt. I needed to use some ad-hoc GUI instead of my text editor, and some stuff had to be typed as comments in one language embedded inside another language that auto-generated the code outside the comment. That part was really gross. Not to mention the whole language looks like a pascal’s ugly cousin, which is superficial but just exaggerated the effect.
It’s really a shame, because I do understand the value proposition, and would wish to harness it. But if authors and fans want their ideas to be widely adopted, they need to make their software work like any other mainstream dev toolchains that developers are used to.
I would love to see “TLA+ for developer”, with a compiler, LSP, modern syntax, maybe even as a library on top of some mainstream programming language. If there is such a thing, or someone is aware of better approaches for the Unix hacker to get into it, I would appreciate it.
Last time I used TLA+, I added support for running the tools from the Emacs mode at https://github.com/mrc/tla-tools. Since there’s a TLA+ tree-sitter grammar now, I might add that next time I use TLA+.
I think that a unix hacker able to “understand the value proposition” could go past the innocuous idiosyncracies of TLA+. I mean, there’s a command line tool that has existed and worked consistently since far before LSP (and even possibly eclipse). Then there’s a fully functioning eclipse environment (so not a basic editor, even if it’s outdated). All this to write models that are usually less than 2 Kloc anyway. And in return you get one of the most important achievements in formal specification and verification of distributed algorithms.
There’s now a vscode plug-in you can use instead of the gui, and a C-style syntax for pluscal. Also, consider looking into Quint as a take on “modern tla+”
I’m mostly with you on this. I’ve used TLA+ in anger a few times with great results but it is definitely a weird experience using the tool.
If anyone reading this is genuinely considering putting the effort in on this… I do have one request: I, personally, enjoy TLA+ and don’t have much of an appetite for PlusCal. But what I would love is something that makes modelling state machines/state charts a little bit easier in TLA+. It’s totally doable as-is, all of the models I’ve built have been parallel-running state machines with message passing between them, but it sure feels like there could be an easier way to write them out.
“Adjective first” is one of my least favorite parts of English. Even as a native speaker, I find it terribly awkward to have to buffer all of the adjectives in my mind before I hear what the noun is that they’re applied to: “the big fluffy white … dog”
Like ISO 8601 dates, this article is correct to say that the noun should go first and all modifiers/adjectives come after.
Even more fun, “big fluffy white dog” is canonical and other adjective orderings like “white fluffy big dog” are incorrect! And adjective ordering is not universal across languages, or even for some closely related languages.
Many adjective second languages aren’t exclusively adjective second either. In Spanish, “zapatos viejos” means “old shoes,” but “viejos zapatos” means “OLD shoes” (i.e. emphasis on old).
For an unspecced language like English, both “canonical” and “incorrect” raise the descriptivist’s ire in me.
Further to your second point, many languages differ on whether certain concepts are expressed using adjectives or other parts of speech, or whether they even separate them cleanly.
Other adjective orderings “feel wrong” to virtually all native English speakers, even though most speakers are completely unaware the rule exists.
If descriptive linguistics didn’t care about “canonical” and “incorrect” then the field would be extremely shallow. “Just like, say any words dawg. Believed by all, eye of, within is held correctness, the beholder’s semantics irrelevant linguists!” You can probably piece together what that’s supposed to mean but it’s most definitely incorrect.
Yet you still said the canonical “big fluffy white dog” instead of any of those other orderings, as the vast majority of native speakers would. Other adjective orders aren’t incorrect because they’re bad, they’re incorrect because descriptively those orders are almost never used in practice.
Put another way, if a non-native English speaker wanted to sound more natural to the widest audience, they would learn the correct ordering, even though the meaning of their words would be perfectly clear out of order.
Yet you still said the canonical “big fluffy white dog” instead of any of those other orderings
? I think you’re mixing up me and who you replied to initially. Your point is not made.
edit: to be clear, the one I’d most likely use (though it’s hard to say now for sure, obviously!) is “big white fluffy dog”. Why? I enjoy dogs a lot, and “fluffy dog” a bit of a unit in my mind. “big fluffy white dog” sounds ever so slightly awkward. “big dog” is also a bit of a semantic unit in my mind, and I could see those going together, though at that stage it’d probably become “fluffy white big dog”.
Ah yes, I did mix you two up. Either way, that is the way most people will say it in normal circumstances. My mix up doesn’t change that adjective ordering is well understood by linguists.
The “wrong” adjective orderings aren’t necessarily “incorrect” in English. Intentional atypical order is used to change meaning. It can split adjectives and what they apply to.
They are incorrect if used unintentionally. Although now we are splitting hairs over exactly what “incorrect” means, and I think we both agree there is a “typical” and “atypical” ordering.
Then in the example, should it become ScreenFull.tsx too? UserCurrent? Using the English order, those names are not ordered, sure, but at least it doesn’t sound like gibberish phrasing. Maybe it’s just a habit though.
If I imagine further, UserCurrent.tsx sitting right next to User.tsx doesn’t seem so bad.
ScreenFull.tsx seems a little silly, but I feel that’s because — unless there’s also other kinds of Screens — FullScreen is being used as an adjective in its wholeness (or adverb perhaps), i.e. “this is the component we use when we go full-screen”, as opposed to “this is the full screen, and this is the empty one”.
I spotted that, and I think it applies best to ButtonGoLive.tsx, since you’re likely to have more buttons than screens.
I don’t honestly have a strong opinion on Noun-Adjective vs Adjective-Noun (vs Noun-Verb, Verb-Noun, Noun-Adjective-Verb, …..). Most have their merits and it seems largely a matter of taste.
That said, I think it’s a vital part of any code style guide. As long as the codebase is consistent, the discoverability boon is substantial. As soon as it’s not standardized, finding anything becomes a chore.
At least English is reasonably consistent about adjective-first. Some “noun-first” languages require you to memorize special exceptions for some adjectives that come first despite the general rule:
Français: « Il y a un petit chien dans ce joli café »
Español: “El otro hombre está aquí”
etc.
(Spanish is actually quite annoying in that you can flip the order of a bunch of otherwise postpositive adjectives for emphasis or “poetic” reasons; French at least just kinda has its list of exceptions and once you know them you know them)
French-native speaker here. What you’re saying about the French language is erroneous. Most adjectives tend to appear after the name, but there’s no general rule. Additionally, the position of the adjective may change the meaning , e.g. “un homme grand is a tall man while”un grand homme” is a “great man”.
Part of my comment was meant to be joking/exaggerating for humor, but I will say my genuine experience with both languages is that Spanish and Spanish speakers are much more flexible with word order than French and French speakers.
The complexity in French, for me as non-native speaker, is the large number of irregular verbs, the inconsistencies of the pronunciation/spelling, and the more complex gender/number agreement. Spanish verbs are much more regular, Spanish pronunciation is much more regular, and Spanish gender/number agreement is simpler. But then Spanish is complex in its flexibility, playing with word order and completely dropping many pronouns and even nouns.
The exact opposite I think. Formal verification is the process of explicitly figuring out what invariants the code relies on, what invariants the code upholds, and testing that those are the same.
If Hubris was formally verified, the invariant that loaned memory would fit into one region would have been written down as a part of the proof of correctness, and when that invariant was changed the tooling would have told them that the code relying on it was no longer correct.
In critical software land, such as avionics (e.g. DO-178C), and indeed systems/quality engineering generally in many industrial settings, the emphasis is on V&V (as contrasted to a solitary V), which is Validation and Verification. Validation is actually making sure that your requirements/specification correctly capture what is required by the end user (the bit that was missing here, un uncaptured invariant), and Verification is the process of making sure that the software performs according to the specification.
You need both! They can’t really exist in isolation. We have a slight annoyance in the current state of computer science that you have to use a specific language like TLA+ to check that a slightly lower level specification (e.g. memory allocation) cannot put the system into a state where it violates a set of rules about the system behaviour, before then having to implement that specification in, say, rust, with a completely independent effort to make sure the rust is doing the same thing as the TLA. There is a whole layer of real-world stuff on top for many practical problems, like it’s hard to capture JPL using Metric and Lockheed using Imperial on their shared Mars mission, but it’s more just layers of an onion with different intermediate languages and varying levels of messy human-factor/organizational-behavior things to capture and specify in different layers; but it’s all still just V&V and it absolutely applies to the real world.
#lobsters was chatting about the similarities between Ruby’s &., Javascript’s ?., Haskell’s Maybe, and Rust’s Option. I remembered this book and was delighted to see it’s now freely available. It’s a favorite of mine, I really like this style of reintroducing familiar concepts to thoughtfully contrast ways that different tools address a problem. This book explores how things Ruby and Haskell differ on handling nulls, which boils down to whether it’s a language feature that’s concise and idiomatic or a design pattern you have to be perfectly diligent about (or, sometimes, can enforce with a linter).
They should have also added Scala 3 to the list. Since in Scala 3 there are two ways to deal with it: one is using Option which is pretty much copied from Haskell (and got then copied by Rust). But they also have union types like Int | Null. I don’t know any known language that has both (unless esotheric typescript libraries are counted in) and it’s interesting to see how both patterns apply to different problems.
First a nitpick: I would argue that Scala, at least when it appeared, was strongly inspired by OCaml; the latter has an option type.
More importantly, for reference, OCaml has had polymorphic variants for around 25 years. Rewriting this Scala doc example:
type username = [ `Name of string ]
type password = [ `Hash of int ]
let help (id : [< username | password]) = match id with
| `Name name -> "hello " ^ name
| `Hash i -> string_of_int i
Now polymorphic variants are not union types per se as, in particular, they can only be united to other polymorphic variants (and not to any type). I don’t know if it’s the same situation for Scala.
Finally, notice that OCaml is even a bit stronger than what I showed as types can be inferred. In the example above, we don’t want that (hence the type definitions and annotation in help) as we must prevent adding a third case to help (as in the Scala example).
First a nitpick: I would argue that Scala, at least when it appeared, was strongly inspired by OCaml; the latter has an option type.
Fair enough - I’m not sure where the inspiration came from, but I guess it also doesn’t matter much.
Now polymorphic variants are not union types per se as, in particular, they can only be united to other polymorphic variants (and not to any type). I don’t know if it’s the same situation for Scala.
It’s not the same in Scala because Scala has subtyping. It makes a huge difference. I’m not saying that it’s better but it allows for very different patterns. At least I would argue it is much more expressive. It comes at quite a price in terms of language complexity though.
I’m not sure to understand because, that was the point of my reply, OCaml has a form of subtyping for polymorphic variants (unions and subtyping go hand in hand anyway). To be clear, notice that these are different from plain variants (aka sum types).
Since in Scala 3 there are two ways to deal with it: one is using Option which is pretty much copied from Haskell (and got then copied by Rust).
Option in Rust comes from SML via OCaml. It was proposed in 1994 in “A New Initial Basis for Standard ML”, but I imagine it must have been in use before that. Scala also no doubt was inspired by SML. Haskell’s Maybe seems to come into Haskell in 1996 in the Haskell 1.3 Report, but again I’d imagine it was a common pattern and was around before that. I don’t think it’s fair to call any of this copying, these are common threads through languages, building on each other’s patterns and idioms.
This is called “smart constructors” in the functional programming community, and indeed a well-known technique there. (For example, if you implement regular expressions using derivatives, you want to use smart constructors to perform simplification on the fly to avoid size blowup.)
To me it seems like it doesn’t really deserve a name … It’s literally just “functions” in this JavaScript code. There are no objects in the OOP sense, like in Python or C++.
So I don’t know why just using functions and records should deserve a special name. Functions are allowed to have logic to create records :) I do that all the time, outside this context of expression simplification.
Smart constructors are just functions that build values of the required type, but perform some extra checks when the value is constructed
I guess the name “constructor” may refer to the variant in a sum type, not an OOP “constructor”. But that doesn’t even seem accurate, because you can have a “smart constructor” for a plain record too.
I think the Haskell definition is a bit imprecise. Usually, in FP, you have one smart constructor per means to build (“construct”) a value of a type. The said means indeed corresponds to a variant or to a record (or other apparatus if there is such). Its aim is usually to ensure an invariant or to perform some “smart” optimization.
Such a function can arguably considered different from other functions which observe data, destruct it, or even build complex data. I think part of this classification can be related to the theory of abstract data types.
There was some interest in Z notation at my school (New Mexico Tech) because it was the formalism Allan Stavely used in his book Towards Zero-Defect Programming and in some versions of his course on the topic of “cleanroom programming.” He made it clear that other notations could be used but I don’t think he did. The approach amounts to write the formal specification, break it down into smaller pieces, prove that the smaller pieces implement the larger ones, and then write code that performs the smaller pieces, and then prove that the code matches those pieces.
He purportedly shopped this around to places like IBM but I have never really found anyone who encountered this stuff “in the wild.” As you might predict, students found this rather tedious and I only know one example of a practitioner who adopted it pervasively, and he passed away a few years ago.
Anyway, I have a few books on Z notation and I find the notation kind of pleasing. I would like to know more about what the successors are, and if they’re used more, and what it is about Z that makes it worse than successor languages. I suspect that a big one is simply that Z wasn’t fully formal, there were no Z compilers or checkers, but I’d like to know what @hwayne has to say about it.
You’re right. Z was just too big and complex for contemporaries to build compilers or checkers. B and Alloy are more restricted languages, which makes them feasible to check.
AFAIK Z has been used in industrial applications, notably by (what is called nowadays) Altran UK, carrying the implementation with Spark Ada.
I’d rather call Z or B set-theoretical as they feature the “element of” operator (btw, Z comes from Zermelo and B from Bourbaki of set-theoretic fame). B itself is can be partly seen as an extension of GCL, so suitable for sequential programs, while Event-B can be seen as an extension of state machines to model “systems”.
On the other hand Alloy (pre-v6) is indeed relational as the only objects manipulated by formulas are relations. I would have put Alloy v6 in the same section as TLA+ as it features all operators of LTL with Past (TLA+ is more restricted in this respect, notably to allow the use of proof techniques rather than model-checking).
The most impressive applications of formal methods I know, going down to an implementation running daily, are (1) the automated braking system of Paris metro line 14 “METEOR” (IIRC: 80K+ lines of proven B code, already in 1998; updated since then for metros all over the world, the code is now more than 200K lines of B AFAIK) and (2) the Scade/Lustre/Esterel-based fly-by-wire flight control system of Airbuses A320s and later.
I reread your comment and I honestly can’t tell what i meant :D.
I think on first read it sounded like you were asking if Z were mentioned, and it was briefly mentioned under the relational algebra section. But, on second read, it sounds like you just want to know why Z isn’t used much in practice.
My take on that is, it’s not used because Z has no tactile connection to executable code - “the verification gap” - and this severely limits its utility. It is absolutely a great tool for thinking, I really like reading Z specs, but you just can’t do anything with them.
Conversely, I really think the only reason anyone uses TLA+ at all is because of the model checker. It at least makes specification tactile - you can interact with and ‘execute’ the spec, and check it for different properties.
Leslie Lamport would probably be upset at that, because TLA+ can model specs that can’t be checked by the model checker, and it has no goal of being executable at all. It just so happens that a good subset of it is model checkable and executable. But, I think it’s the truth, and I think specification languages need some kind of executability to ever have a hope of being used in practice.
Nice example. For teaching, I like to use this small variation of it, relying on the classical duality between between && and ||. The idea is to state that what you want is that it’s impossible for a to be administrator without activating 2FA. Said otherwise, you want !(Admin(a) && !2FA(A)), that is !Admin(a) || 2FA(a). Which is how we define Admin(a) => 2FA(a).
Regarding style and tone: this is incredibly well-written and the examples are simple enough to be tractable but rich enough to stay illustrative. I felt like I could follow the article appropriately even if some of the finer points remain above my head. Hopefully diving in and doing some sketching will help that. Well done, @hwayne.
Regarding the substance and content: I am very excited to dig into Alloy 6 and very curious how the new book by the Alloy team will shape up. In particular, I wonder how they will position Alloy relative to other tools in the space where TLA+, is only one example.
I’ve used Alloy in the past and feel strongly that my time with it was productive, particularly when I formally specified an algebra I’ve been working on for some time to get the structures right. These new temporal aspects will only improve my ability to specify it by adding a whole new dimension. Curious what other users think.
I’m one of the Alloy 6 authors. As far as I know, there are not so many mature formal tools that can nicely be used to specify both structural and causal aspects of a system (that is, mixing first-order and temporal reasoning). So I’d say TLA+ (which we also use, mainly in teaching but also for some research work) remains the principal object of comparison. If you want to model an algorithm that you can express easily in PlusCAL (e.g. an algorithm with many sequential parts and interruptions at various points) or if you want to carry out full proofs (there is an Isabelle backend for this), then TLA+ is a tool of choice.
It is therefore not very relevant for Alloy to address the exact same problems as TLA+. Our main focus has rather been to try to improve Alloy’s own strengths, in particular the fact it’s really good to model and analyze requirements or high-level designs, and to find flaws quickly and automatically. Indeed (1) the language is quite flexible (thanks to the ability to state -no pun intended- global, temporal properties about your system); (2) the variety of temporal connectives (incl. past ones) can be handy for some properties (e.g. “in any state, a node in a ring is elected as a leader if and only iff it has received its own address”: always all n: Node | n in Elected iff once (n.address in n.mailbox)); (3) model finding is performed up to a user-specified bound and the tool leverages the fact that some objects are constant or mutable to improve efficiency; and (4) finally the Visualizer is really nice, in particular with its new trace exploration capabilities.
First, thanks for responding. Second, thank you SO much for all your hard work. Your many efforts have been noticed and noted by many appreciative folks. Congrats on the release and occasion!
It is therefore not very relevant for Alloy to address the exact same problems as TLA+.
Your explanation from the previous paragraph makes this conclusion follow very closely and I think I get your point about this bit:
Our main focus has rather been to try to improve Alloy’s own strengths, in particular the fact it’s really good to model and analyze requirements or high-level designs, and to find flaws quickly and automatically.
I have had some difficulty introducing Alloy at me workplace but the following is growing. Luckily my selling points are consistent with the high-level design practices associated with iterative specification. I have a funky name for it so it sounds acceptable to corporate ears but “Test-Drive Architecture” and associated terminology isn’t particularly descriptive.
Again, thanks a ton for your efforts and reply. Feel free to reach out if you’re interested in further dialog. Wishing you and the team the best!
It is therefore not very relevant for Alloy to address the exact same problems as TLA+.
Your explanation from the previous paragraph makes this conclusion follow very closely and I think I get your point about this bit:
I probably wasn’t very clear here. What I meant is that there’s added value in expanding what Alloy is already particularly good at (namely scenario exploration and quick bug-finding in designs, all in a user-friendly language and tool). While if you have the kind of problems for which TLA+ already shines, you should most certainly use TLA+.
Yes, but I can also say that your aside on how TL is hard made me feel better. Right at home, even.
I think most of the time the finer points of Alloy itself go over my head when I can’t remember just what exactly the transitive closure of a relation does! Is that sufficient or would quotations help more?
It’s a bit misleading since the download page still mentions that the latest available version is Alloy 5, but the link to the latest build actually targets the version 6.0.0. Ideally this should be updated. In anyway I can’t wait to give it a try, the last time I attempted to use Alloy to model something serious I struggled a lot to deal with time. These new additions look great!
Hi, I’m one of the authors of this addition to Alloy. Indeed, the site ins’t fully up-to-date yet but it should be soon. This version of Alloy is a rebranding/reshaping of an open-source extension code-named Electrum, that we’ve been developing and using for several years. I think the summary by Hillel is right on the nose. Feel free to ask any question.
I like Alloy, especially after they added the new temporal features in version 6.
Last time I played with it, it had to be used from inside some awful IDE though. I know this is a common complaint, my point is not to repeat it. What I wanted to say is that while I was browsing the download page for Alloy just now, I noticed that it links to Sterling: A Web-based Visualizer for Relational Modeling Languages. I was hoping it would allow me to use my own editor and do custom visualisations in a browser, this doesn’t seem to be the case, rather it’s a new web-based IDE.
However, as I was skimming through the Sterling paper, I noticed that it said that Sterling also “is the visualizer for an Alloy-like model finder called Forge, which is being developed at Brown University and is used to teach a Logic for Systems class of over 60 students”. So I looked up Forge, it appears to be a Racket “language”/eDSL which looks like Alloy. I’m still not sure what the exact difference is, their readme says “Forge is heavily adapted from the excellent Alloy, a more widely used and somewhat more scalable tool. Forge and Alloy even use the same engines!”, but also “For broader historical context on Forge, the Alloy documentation or an Alloy demo may be useful. We don’t suggest using these as reference for Forge itself, however.”. In either case, it seems Forge might be a way to get a taste of Alloy without the sour taste of their IDE!
Hi, I’m one of the authors of Alloy 6 and of this new book.
I think the image of the Alloy Analyzer your depicting is a bit too dark. The IDE is quite sophisticated since it features an interconnection of a solving engine, a rich visualizer as well as a very useful evaluator (to navigate instances and counterexamples). Compared with other formal methods, I think Alloy is quite good in terms of user-friendliness and usefulness of results it provides. The legacy integrated editor is on the other hand quite basic but, considering models in Alloy are rather small, the -real- annoyances remain limited in my view (the editor has syntax highlighting, error reporting, find&replace…). An interesting aspect for non-power users is that this is all delivered in a single, ready-to-run JAR file. This is in particular invaluable with students (Alloy is taught in several universities, at least in Europe and in America).
A future version will allow users to rely on LSP and use an editor of their choice (there were already some experiments with LSP and there actually is an unofficial VSCode plugin but it’s not up to date). As an “epxert” user myself, what I would not want, however, would be to lose the the above-mentioned sophisticated interactions present in the tool, for the sake of getting a slicker editing experience.
Alloy 6.2 now has a command line but it’s not that great for solving, more for automated build chains. Many serious Alloy users I know use the Vscode extension.
The new A6.2 command line indeed allows to execute the same kinds commands than in the GUI, with roughly the same options, so it’s mainly aimed at facilitating batch verification and benchmarks, I’d say.
For people who do not know the Alloy Analyzer completely, this is different from the Evaluator feature mentioned above, which allows to query, in Alloy itself, an instance or counter-example currently being shown by the Visualizer. This feature, which isn’t new by the way, is very useful in practice when models become complex.
Finally, the VSCode extension does not use Alloy analyzer 6.1 nor 6.2 but it ships a tailored version, AFAIK. It’s indeed already great but, hopefully, in the future, we will be able to get a plugin that can connect to the “real”, official Alloy.
The main thing refraining me to use tools other than pdflatex+bibtex is that they don’t seem to be compatible with the requirements of scientific editors. How do other scientists address this?
Typst has a proven track record of being able to imitate the style of various scientific journals. It seems reasonable to bet that even if your particular template is not currently supported, someone could port it. So you could either wait for someone else to do it, or try doing it yourself.
I would be curious to give Typst a try, and my idea is to start with some area where style requirements are less stringent: grant proposals for example, but actually I would like to try it for slides. I find beamer unpleasantly heavy to use. I often prototype my slides in Markdown first, and I think that Typst could remove this intermediate step and provide a pleasant experience thanks to live rendering. (Re. live rendering: texpresso provides live rendering for LaTeX, and it does improve things noticeably for beamer slides.)
That said, some tools expect LaTeX sources as part of their pipeline – arXiv for example expects “sources” and it means LaTeX, and they built a lot of custom tooling to work with the TeX sources. I don’t think they will be usable with Typst for a long while, except maybe if people were to find a way to write a good-enough translator from Typst to LaTeX.
Typst has a proven track record of being able to imitate the style of various scientific journals. It seems reasonable to bet that even if your particular template is not currently supported, someone could port it. So you could either wait for someone else to do it, or try doing it yourself.
I would be curious to give Typst a try, and my idea is to start with some area where style requirements are less stringent: grant proposals for example, but actually I would like to try it for slides. I find beamer unpleasantly heavy to use. I often prototype my slides in Markdown first, and I think that Typst could remove this intermediate step and provide a pleasant experience thanks to live rendering. (Re. live rendering: texpresso provides live rendering for LaTeX, and it does improve things noticeably for beamer slides.)
That said, some tools expect LaTeX sources as part of their pipeline – arXiv for example expects “sources” and it means LaTeX, and they built a lot of custom tooling to work with the TeX sources. I don’t think they will be usable with Typst for a long while, except maybe if people were to find a way to write a good-enough translator from Typst to LaTeX.
Last time I tried to use TLA+ I got very much repulsed by how hacky and amateurish it felt. I needed to use some ad-hoc GUI instead of my text editor, and some stuff had to be typed as comments in one language embedded inside another language that auto-generated the code outside the comment. That part was really gross. Not to mention the whole language looks like a pascal’s ugly cousin, which is superficial but just exaggerated the effect.
It’s really a shame, because I do understand the value proposition, and would wish to harness it. But if authors and fans want their ideas to be widely adopted, they need to make their software work like any other mainstream dev toolchains that developers are used to.
I would love to see “TLA+ for developer”, with a compiler, LSP, modern syntax, maybe even as a library on top of some mainstream programming language. If there is such a thing, or someone is aware of better approaches for the Unix hacker to get into it, I would appreciate it.
Last time I used TLA+, I added support for running the tools from the Emacs mode at https://github.com/mrc/tla-tools. Since there’s a TLA+ tree-sitter grammar now, I might add that next time I use TLA+.
I think that a unix hacker able to “understand the value proposition” could go past the innocuous idiosyncracies of TLA+. I mean, there’s a command line tool that has existed and worked consistently since far before LSP (and even possibly eclipse). Then there’s a fully functioning eclipse environment (so not a basic editor, even if it’s outdated). All this to write models that are usually less than 2 Kloc anyway. And in return you get one of the most important achievements in formal specification and verification of distributed algorithms.
There’s now a vscode plug-in you can use instead of the gui, and a C-style syntax for pluscal. Also, consider looking into Quint as a take on “modern tla+”
Oh, Quint looks so nice. Thanks!
There’s also P (https://p-org.github.io/P/), I would be interested in hearing your opinion on that
I’m mostly with you on this. I’ve used TLA+ in anger a few times with great results but it is definitely a weird experience using the tool.
If anyone reading this is genuinely considering putting the effort in on this… I do have one request: I, personally, enjoy TLA+ and don’t have much of an appetite for PlusCal. But what I would love is something that makes modelling state machines/state charts a little bit easier in TLA+. It’s totally doable as-is, all of the models I’ve built have been parallel-running state machines with message passing between them, but it sure feels like there could be an easier way to write them out.
“Adjective first” is one of my least favorite parts of English. Even as a native speaker, I find it terribly awkward to have to buffer all of the adjectives in my mind before I hear what the noun is that they’re applied to: “the big fluffy white … dog”
Like ISO 8601 dates, this article is correct to say that the noun should go first and all modifiers/adjectives come after.
Even more fun, “big fluffy white dog” is canonical and other adjective orderings like “white fluffy big dog” are incorrect! And adjective ordering is not universal across languages, or even for some closely related languages.
Many adjective second languages aren’t exclusively adjective second either. In Spanish, “zapatos viejos” means “old shoes,” but “viejos zapatos” means “OLD shoes” (i.e. emphasis on old).
For an unspecced language like English, both “canonical” and “incorrect” raise the descriptivist’s ire in me.
Further to your second point, many languages differ on whether certain concepts are expressed using adjectives or other parts of speech, or whether they even separate them cleanly.
Other adjective orderings “feel wrong” to virtually all native English speakers, even though most speakers are completely unaware the rule exists.
If descriptive linguistics didn’t care about “canonical” and “incorrect” then the field would be extremely shallow. “Just like, say any words dawg. Believed by all, eye of, within is held correctness, the beholder’s semantics irrelevant linguists!” You can probably piece together what that’s supposed to mean but it’s most definitely incorrect.
Is it “canonical incorrect version” or “incorrect canonical version”? :P
I only made the point because several other orderings of those particular adjectives don’t feel wrong to me, a native (Australian) English speaker.
(And fair point about “canonical” and “incorrect”—I just felt they were a bridge too far as applied here.)
Yet you still said the canonical “big fluffy white dog” instead of any of those other orderings, as the vast majority of native speakers would. Other adjective orders aren’t incorrect because they’re bad, they’re incorrect because descriptively those orders are almost never used in practice.
Put another way, if a non-native English speaker wanted to sound more natural to the widest audience, they would learn the correct ordering, even though the meaning of their words would be perfectly clear out of order.
? I think you’re mixing up me and who you replied to initially. Your point is not made.
edit: to be clear, the one I’d most likely use (though it’s hard to say now for sure, obviously!) is “big white fluffy dog”. Why? I enjoy dogs a lot, and “fluffy dog” a bit of a unit in my mind. “big fluffy white dog” sounds ever so slightly awkward. “big dog” is also a bit of a semantic unit in my mind, and I could see those going together, though at that stage it’d probably become “fluffy white big dog”.
Ah yes, I did mix you two up. Either way, that is the way most people will say it in normal circumstances. My mix up doesn’t change that adjective ordering is well understood by linguists.
Why the green great dragon can’t exist.
Maybe “opinion-size-age-shape-colour-origin-material-purpose” is different in Australia?
Is “fluffy” a shape, or a material? :3
The “wrong” adjective orderings aren’t necessarily “incorrect” in English. Intentional atypical order is used to change meaning. It can split adjectives and what they apply to.
Big Blue House parses as (Big and Blue) (House)
Blue Big House parses as (Blue) (Big House)
They are incorrect if used unintentionally. Although now we are splitting hairs over exactly what “incorrect” means, and I think we both agree there is a “typical” and “atypical” ordering.
My brain wants to say “big white fluffy dog”, interestingly.
Then in the example, should it become
ScreenFull.tsxtoo?UserCurrent? Using the English order, those names are not ordered, sure, but at least it doesn’t sound like gibberish phrasing. Maybe it’s just a habit though.If I imagine further,
UserCurrent.tsxsitting right next toUser.tsxdoesn’t seem so bad.ScreenFull.tsxseems a little silly, but I feel that’s because — unless there’s also other kinds ofScreens —FullScreenis being used as an adjective in its wholeness (or adverb perhaps), i.e. “this is the component we use when we go full-screen”, as opposed to “this is the full screen, and this is the empty one”.I spotted that, and I think it applies best to
ButtonGoLive.tsx, since you’re likely to have more buttons than screens.I don’t honestly have a strong opinion on
Noun-AdjectivevsAdjective-Noun(vsNoun-Verb,Verb-Noun,Noun-Adjective-Verb, …..). Most have their merits and it seems largely a matter of taste.That said, I think it’s a vital part of any code style guide. As long as the codebase is consistent, the discoverability boon is substantial. As soon as it’s not standardized, finding anything becomes a chore.
At least English is reasonably consistent about adjective-first. Some “noun-first” languages require you to memorize special exceptions for some adjectives that come first despite the general rule:
Français: « Il y a un petit chien dans ce joli café »
Español: “El otro hombre está aquí”
etc.
(Spanish is actually quite annoying in that you can flip the order of a bunch of otherwise postpositive adjectives for emphasis or “poetic” reasons; French at least just kinda has its list of exceptions and once you know them you know them)
French-native speaker here. What you’re saying about the French language is erroneous. Most adjectives tend to appear after the name, but there’s no general rule. Additionally, the position of the adjective may change the meaning , e.g. “un homme grand is a tall man while”un grand homme” is a “great man”.
Part of my comment was meant to be joking/exaggerating for humor, but I will say my genuine experience with both languages is that Spanish and Spanish speakers are much more flexible with word order than French and French speakers.
The complexity in French, for me as non-native speaker, is the large number of irregular verbs, the inconsistencies of the pronunciation/spelling, and the more complex gender/number agreement. Spanish verbs are much more regular, Spanish pronunciation is much more regular, and Spanish gender/number agreement is simpler. But then Spanish is complex in its flexibility, playing with word order and completely dropping many pronouns and even nouns.
the same is true for english
Or in other words, formal verification doesn’t apply to systems modelling real world.
The exact opposite I think. Formal verification is the process of explicitly figuring out what invariants the code relies on, what invariants the code upholds, and testing that those are the same.
If Hubris was formally verified, the invariant that loaned memory would fit into one region would have been written down as a part of the proof of correctness, and when that invariant was changed the tooling would have told them that the code relying on it was no longer correct.
What does it have to do with formal verification?
In critical software land, such as avionics (e.g. DO-178C), and indeed systems/quality engineering generally in many industrial settings, the emphasis is on V&V (as contrasted to a solitary V), which is Validation and Verification. Validation is actually making sure that your requirements/specification correctly capture what is required by the end user (the bit that was missing here, un uncaptured invariant), and Verification is the process of making sure that the software performs according to the specification.
You need both! They can’t really exist in isolation. We have a slight annoyance in the current state of computer science that you have to use a specific language like TLA+ to check that a slightly lower level specification (e.g. memory allocation) cannot put the system into a state where it violates a set of rules about the system behaviour, before then having to implement that specification in, say, rust, with a completely independent effort to make sure the rust is doing the same thing as the TLA. There is a whole layer of real-world stuff on top for many practical problems, like it’s hard to capture JPL using Metric and Lockheed using Imperial on their shared Mars mission, but it’s more just layers of an onion with different intermediate languages and varying levels of messy human-factor/organizational-behavior things to capture and specify in different layers; but it’s all still just V&V and it absolutely applies to the real world.
That doesn’t feel like a very helpful formulation. They must apply to some extent, or they wouldn’t be used and wouldn’t be useful.
#lobsters was chatting about the similarities between Ruby’s
&., Javascript’s?., Haskell’sMaybe, and Rust’sOption. I remembered this book and was delighted to see it’s now freely available. It’s a favorite of mine, I really like this style of reintroducing familiar concepts to thoughtfully contrast ways that different tools address a problem. This book explores how things Ruby and Haskell differ on handling nulls, which boils down to whether it’s a language feature that’s concise and idiomatic or a design pattern you have to be perfectly diligent about (or, sometimes, can enforce with a linter).They should have also added Scala 3 to the list. Since in Scala 3 there are two ways to deal with it: one is using
Optionwhich is pretty much copied from Haskell (and got then copied by Rust). But they also have union types likeInt | Null. I don’t know any known language that has both (unless esotheric typescript libraries are counted in) and it’s interesting to see how both patterns apply to different problems.First a nitpick: I would argue that Scala, at least when it appeared, was strongly inspired by OCaml; the latter has an
optiontype.More importantly, for reference, OCaml has had polymorphic variants for around 25 years. Rewriting this Scala doc example:
Now polymorphic variants are not union types per se as, in particular, they can only be united to other polymorphic variants (and not to any type). I don’t know if it’s the same situation for Scala.
Finally, notice that OCaml is even a bit stronger than what I showed as types can be inferred. In the example above, we don’t want that (hence the type definitions and annotation in
help) as we must prevent adding a third case tohelp(as in the Scala example).Fair enough - I’m not sure where the inspiration came from, but I guess it also doesn’t matter much.
It’s not the same in Scala because Scala has subtyping. It makes a huge difference. I’m not saying that it’s better but it allows for very different patterns. At least I would argue it is much more expressive. It comes at quite a price in terms of language complexity though.
I’m not sure to understand because, that was the point of my reply, OCaml has a form of subtyping for polymorphic variants (unions and subtyping go hand in hand anyway). To be clear, notice that these are different from plain variants (aka sum types).
Optionin Rust comes from SML via OCaml. It was proposed in 1994 in “A New Initial Basis for Standard ML”, but I imagine it must have been in use before that. Scala also no doubt was inspired by SML. Haskell’sMaybeseems to come into Haskell in 1996 in the Haskell 1.3 Report, but again I’d imagine it was a common pattern and was around before that. I don’t think it’s fair to call any of this copying, these are common threads through languages, building on each other’s patterns and idioms.This is called “smart constructors” in the functional programming community, and indeed a well-known technique there. (For example, if you implement regular expressions using derivatives, you want to use smart constructors to perform simplification on the fly to avoid size blowup.)
To me it seems like it doesn’t really deserve a name … It’s literally just “functions” in this JavaScript code. There are no objects in the OOP sense, like in Python or C++.
So I don’t know why just using functions and records should deserve a special name. Functions are allowed to have logic to create records :) I do that all the time, outside this context of expression simplification.
e.g. https://wiki.haskell.org/Smart_constructors
I guess the name “constructor” may refer to the variant in a sum type, not an OOP “constructor”. But that doesn’t even seem accurate, because you can have a “smart constructor” for a plain record too.
I think the Haskell definition is a bit imprecise. Usually, in FP, you have one smart constructor per means to build (“construct”) a value of a type. The said means indeed corresponds to a variant or to a record (or other apparatus if there is such). Its aim is usually to ensure an invariant or to perform some “smart” optimization.
Such a function can arguably considered different from other functions which observe data, destruct it, or even build complex data. I think part of this classification can be related to the theory of abstract data types.
There was some interest in Z notation at my school (New Mexico Tech) because it was the formalism Allan Stavely used in his book Towards Zero-Defect Programming and in some versions of his course on the topic of “cleanroom programming.” He made it clear that other notations could be used but I don’t think he did. The approach amounts to write the formal specification, break it down into smaller pieces, prove that the smaller pieces implement the larger ones, and then write code that performs the smaller pieces, and then prove that the code matches those pieces.
He purportedly shopped this around to places like IBM but I have never really found anyone who encountered this stuff “in the wild.” As you might predict, students found this rather tedious and I only know one example of a practitioner who adopted it pervasively, and he passed away a few years ago.
Anyway, I have a few books on Z notation and I find the notation kind of pleasing. I would like to know more about what the successors are, and if they’re used more, and what it is about Z that makes it worse than successor languages. I suspect that a big one is simply that Z wasn’t fully formal, there were no Z compilers or checkers, but I’d like to know what @hwayne has to say about it.
You’re right. Z was just too big and complex for contemporaries to build compilers or checkers. B and Alloy are more restricted languages, which makes them feasible to check.
Z and B had the same inventor, too.
AFAIK Z has been used in industrial applications, notably by (what is called nowadays) Altran UK, carrying the implementation with Spark Ada.
I’d rather call Z or B set-theoretical as they feature the “element of” operator (btw, Z comes from Zermelo and B from Bourbaki of set-theoretic fame). B itself is can be partly seen as an extension of GCL, so suitable for sequential programs, while Event-B can be seen as an extension of state machines to model “systems”.
On the other hand Alloy (pre-v6) is indeed relational as the only objects manipulated by formulas are relations. I would have put Alloy v6 in the same section as TLA+ as it features all operators of LTL with Past (TLA+ is more restricted in this respect, notably to allow the use of proof techniques rather than model-checking).
The most impressive applications of formal methods I know, going down to an implementation running daily, are (1) the automated braking system of Paris metro line 14 “METEOR” (IIRC: 80K+ lines of proven B code, already in 1998; updated since then for metros all over the world, the code is now more than 200K lines of B AFAIK) and (2) the Scade/Lustre/Esterel-based fly-by-wire flight control system of Airbuses A320s and later.
Thank you!
In this taxonomy, Z is a relational algebra.
I don’t see how this answers my question. Can you expand on it?
I reread your comment and I honestly can’t tell what i meant :D.
I think on first read it sounded like you were asking if Z were mentioned, and it was briefly mentioned under the relational algebra section. But, on second read, it sounds like you just want to know why Z isn’t used much in practice.
My take on that is, it’s not used because Z has no tactile connection to executable code - “the verification gap” - and this severely limits its utility. It is absolutely a great tool for thinking, I really like reading Z specs, but you just can’t do anything with them.
Conversely, I really think the only reason anyone uses TLA+ at all is because of the model checker. It at least makes specification tactile - you can interact with and ‘execute’ the spec, and check it for different properties.
Leslie Lamport would probably be upset at that, because TLA+ can model specs that can’t be checked by the model checker, and it has no goal of being executable at all. It just so happens that a good subset of it is model checkable and executable. But, I think it’s the truth, and I think specification languages need some kind of executability to ever have a hope of being used in practice.
Thank you, this is very helpful!
Nice example. For teaching, I like to use this small variation of it, relying on the classical duality between between
&&and||. The idea is to state that what you want is that it’s impossible forato be administrator without activating 2FA. Said otherwise, you want!(Admin(a) && !2FA(A)), that is!Admin(a) || 2FA(a). Which is how we defineAdmin(a) => 2FA(a).Regarding style and tone: this is incredibly well-written and the examples are simple enough to be tractable but rich enough to stay illustrative. I felt like I could follow the article appropriately even if some of the finer points remain above my head. Hopefully diving in and doing some sketching will help that. Well done, @hwayne.
Regarding the substance and content: I am very excited to dig into Alloy 6 and very curious how the new book by the Alloy team will shape up. In particular, I wonder how they will position Alloy relative to other tools in the space where TLA+, is only one example.
I’ve used Alloy in the past and feel strongly that my time with it was productive, particularly when I formally specified an algebra I’ve been working on for some time to get the structures right. These new temporal aspects will only improve my ability to specify it by adding a whole new dimension. Curious what other users think.
I’m one of the Alloy 6 authors. As far as I know, there are not so many mature formal tools that can nicely be used to specify both structural and causal aspects of a system (that is, mixing first-order and temporal reasoning). So I’d say TLA+ (which we also use, mainly in teaching but also for some research work) remains the principal object of comparison. If you want to model an algorithm that you can express easily in PlusCAL (e.g. an algorithm with many sequential parts and interruptions at various points) or if you want to carry out full proofs (there is an Isabelle backend for this), then TLA+ is a tool of choice.
It is therefore not very relevant for Alloy to address the exact same problems as TLA+. Our main focus has rather been to try to improve Alloy’s own strengths, in particular the fact it’s really good to model and analyze requirements or high-level designs, and to find flaws quickly and automatically. Indeed (1) the language is quite flexible (thanks to the ability to state -no pun intended- global, temporal properties about your system); (2) the variety of temporal connectives (incl. past ones) can be handy for some properties (e.g. “in any state, a node in a ring is elected as a leader if and only iff it has received its own address”:
always all n: Node | n in Elected iff once (n.address in n.mailbox)); (3) model finding is performed up to a user-specified bound and the tool leverages the fact that some objects are constant or mutable to improve efficiency; and (4) finally the Visualizer is really nice, in particular with its new trace exploration capabilities.First, thanks for responding. Second, thank you SO much for all your hard work. Your many efforts have been noticed and noted by many appreciative folks. Congrats on the release and occasion!
Your explanation from the previous paragraph makes this conclusion follow very closely and I think I get your point about this bit:
I have had some difficulty introducing Alloy at me workplace but the following is growing. Luckily my selling points are consistent with the high-level design practices associated with iterative specification. I have a funky name for it so it sounds acceptable to corporate ears but “Test-Drive Architecture” and associated terminology isn’t particularly descriptive.
Again, thanks a ton for your efforts and reply. Feel free to reach out if you’re interested in further dialog. Wishing you and the team the best!
Thanks, +Jonathan
I probably wasn’t very clear here. What I meant is that there’s added value in expanding what Alloy is already particularly good at (namely scenario exploration and quick bug-finding in designs, all in a user-friendly language and tool). While if you have the kind of problems for which TLA+ already shines, you should most certainly use TLA+.
(Thanks for the appreciation.)
Thanks for the followup!
Can I ask which finer points went over your head? It’s good feedback for me.
Yes, but I can also say that your aside on how TL is hard made me feel better. Right at home, even.
I think most of the time the finer points of Alloy itself go over my head when I can’t remember just what exactly the transitive closure of a relation does! Is that sufficient or would quotations help more?
It’s a bit misleading since the download page still mentions that the latest available version is Alloy 5, but the link to the latest build actually targets the version 6.0.0. Ideally this should be updated. In anyway I can’t wait to give it a try, the last time I attempted to use Alloy to model something serious I struggled a lot to deal with time. These new additions look great!
Hi, I’m one of the authors of this addition to Alloy. Indeed, the site ins’t fully up-to-date yet but it should be soon. This version of Alloy is a rebranding/reshaping of an open-source extension code-named Electrum, that we’ve been developing and using for several years. I think the summary by Hillel is right on the nose. Feel free to ask any question.