agstewart
See discussion here: https://news.ycombinator.com/item?id=26271117
This is from memory, but the TLA+ toolkit distinguishes between your "specification of your algorithm" and a (bounded) "model of your specification".
So, you might have some spec for a sorting function that works for arrays of natural numbers of arbitrary length. And your model would limit it to arrays of length 5, and "define" the natural numbers to be `range(0,10)` -- ie. you are checking a finite "model".
I think this is consistent with the language used in the wiki article (the OP).
> You can see how I'm working against the way TLA wants to work
I'd much prefer your suggested workflow. I don't recall that you can write plain old pcal
It's amusing that you want some TLA CLI tools that work kind of how the LaTex toolkit works, another of Leslie Lamport's contributions...
> I always meant to publish these after XSA-299 went public, but haven't gotten around to it.
Please do!
> It would be nice if I could designate just one file (written in C) whose functions would be translated into TLA. The properties you want to verify about those functions would obviously need to be written in TLA directly.
That seems like a really tractable problem to me, if the C files were written with this in mind. I've actually been thinking about this since giving an internal talk on my TLA+ project last week!
I couldn't find a way of tracking the TLA+ Toolkit's files nicely in git, but with a bit of manual work it's possible, using the `tlc-bin` CLI[0]. I used the TLA+ Toolkit to write the spec[1], but wrote the models by hand (eg. [2]).
This was before I heard of the VS-Code extension. I think it's quite good now, so there might be a better workflow that avoids the TLA+ toolkit altogether.
> What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step.
Do you mean you'd like to generate a TLA+ spec from your source code?
[0] https://github.com/pmer/tla-bin
[1] https://github.com/statechannels/tla-specs/blob/6d7227e2d183...
[2] https://github.com/statechannels/tla-specs/blob/6d7227e2d183...
Magmo is a 100% remote team at Consensys Mesh, focusing on Ethereum state channels research and implementation. State channels (https://statechannels.org/) are a L2 blockchain scaling tool that enables peers to execute many blockchain transactions involving a fixed set of peers, at a fixed cost -- after some initial setup, transactions only involve network messaging. We previously released Web3torrent as a proof of concept (previous discussion: https://news.ycombinator.com/item?id=23602008) and are currently collaborating with The Graph to implement state channels on a large scale on mainnet (https://thegraph.com/blog/the-graph-brings-state-channels-to...).
We're currently hiring a full stack developer, though we will happily consider any candidate with an appropriate background and a keen interest in our project. Our stack includes Typescript, PostgreSQL, Solidity, Rust, and React. We've also used TLA+ for some formal verification (https://blog.statechannels.org/breaking-state-channels/), and aim to use more tools to verify our protocols and implementations.
Full time employment is preferred, though many of our team work part-time, and we are open to flexible working arrangements.
See our job posting at https://consensys.net/open-roles/2510553/, or email me directly (andrew DOT stewart [at] mesh DOT xyz) if you have any questions.
https://deepmind.com/blog/deepmind-ai-reduces-google-data-ce...
Just because alpha zero doesn't solve the problem you want it to doesn't mean that advancements aren't being made that matter to someone else. To ignore that seems disingenuous.