HN Theater @HNTheaterMonth

I've invested a fair amount of time into learning TLA+, have bought Hillel Wayne's book (Practical TLA+), and found his stuff super valuable. However, if I could do it again, I would have started in the following order:

- 1. Watch https://www.youtube.com/watch?v=-4Yp3j_jk8Q

- 2. Watch all of https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7...

- 3. Work through examples on https://learntla.com

I'm normally not a huge fan of YouTube over books / web sites, but in this case the best content comes from Lamport himself, and he's presented it as a YouTube Course. Also, the costume changes are hilarious.

⬐ tunesmith

I watched Lamport's entire video series once and only just felt I was starting to get it. I will have to watch the entire thing again.

I also found a (very minor, inconsequential) bug in the materials and emailed him, and he wrote me back and said thanks, so that felt like a career highlight to me ;)

There is TLA+ for verifying specifications. Here is a talk by its creator:

https://www.youtube.com/watch?v=-4Yp3j_jk8Q

"Writing is nature's way of letting you know how sloppy your thinking is." [1] Dick Guindon

"To think, you have to write. If you're thinking without writing, chances are you're fooling yourself. You're only pretending to think." [1] Leslie Lamport

[1] https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=179s

Coder sees "We need feature X". Coder implements feature X, marks it as complete; next.

So they have the coder (implementer) role covered, but not the "programmer" role ("thinker"/feature designer).

Leslie Lamport - Thinking Above the Code: ~ A lot of people like to think that they're thinking, but they don't really do much thinking. [1]

Evidently, there was no expectation that the coder/implementer was supposed to do any thinking here.

[1] https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=134s

⬐ willcipriano

This got past the undoubtedly upwards of nine product managers/business analysts/directors/etc on the team as well. Blaming the low man on that totem pole in a organization thick with management like that is silly.

None of the "idea men" had the idea of "what if someone's cat walks across the keyboard when we ask them their birthday". That's the embarrassing failure here.

⬐ cdjk

This could actually be a feature and not a bug from a legal perspective. If they are blocking anyone who gives any indication that they are under 13 then it might be easier to show compliance with COPPA.

This has made me wonder at times if the best way to get my data delete from someplace is to talk to customer service and repeatedly say that I'm twelve.

⬐ hansvm

That's definitely how it explicitly worked at one workplace; to the extent that account restrictions could form a poset, if we had evidence that some restriction might be required (e.g., from multiple forms of age evidence, do any of them indicate this might be a minor or some other protected class), that restriction would be applied.

I agree with this perspective.

I think people seeking to automate software development should find out a way of compiling something like TLA+[0] to executable code.

Right now coders are both masons(brick layers) & architects. TLA+ is what can bee seen as a "blueprint" for code, and the actual code can be thought of as the brick and mortar.

Devs having to only focus on the blueprint of the code i.e specifications written in TLA+. Truly takes the industry forward.

[0]: https://www.youtube.com/watch?v=-4Yp3j_jk8Q

⬐ ithkuil

> Right now coders are both masons(brick layers) & architects

Not sure how common this is today, but I do remember the time when software development was done by people writing hundreds of pages of specifications of various level of detail (including class diagrams, method names etc) and then delegating the menial work to very junior folks. In many cases I witnessed true contempt for the mere job of transcribing programs.

I'm not talking of some dark age of punchcards; but clearly learning the boring details of the Java SDK and figuring out how to setup your Eclipse project (let alone using CVS/SVN) was deemed to be below the pay level of many.

The quality of the software produced in those environments was abysmal. I'm not talking about specs on general, but the practice of making the mistake of overspecifying to the extent you think you need a quasi-mechanical transcription (an undergrad student or a very junior dev) but at the same time not really specifying everything and thus le

⬐ OldOneEye

It's a shame your message got cut.

I remember having the same experience during my third job, in a french consultancy in Spain. For the sake of vindication (so many years after the fact xDD) I will just name it: Sopra [0].

So, for each business task (like adding some feature to the application we were developing), "Analysts" would write the "specification" in uml-like models in Eclipse (some kind of modelling plugin for Eclipse, I think it was a framework developed by the company over the EMF plugin suite), and a very short description of what this was supposed to accomplish, business-wise.

Our[1] task would be, then, to generate a scaffolding from these models (via Eclipse) and then to fill in the blank of the methods generated this way.

The problem lay at how the incentives were laid in that company (and many others like it, the whole IT "consultancy"[2] business, in fact) : Programming was a job that was poorly paid (but still, much higher than the median salary in Madrid, which is why I was there). So, every person had every incentive to get to either management or higher "design" roles (Technical Analyst, Business Analyst, Architect) as soon as possible. This meant that the people who remained in the company[3] were either the people that had 1 year, 2 year tops, of programming experience that got to now design whole systems and applications, or the sociopaths that floated to management by stabbing everyone on the way up.

You can imagine the quality of the systems produced this way...

Models were hilariously under specified, and clearly the person doing them did not have experience on how programas behave in real life. But because they were so insecure in their positions (remember the backstabbing and the lack of experience), any back and forth between the programmers and the analysts was handled with hostility and contempt from the analyst side.

Obviously we also looked at analysts with contempt. Still, they were paid better than us, so of course they were right and they had management support, and were told by our team leads to make it work anyway, so it was common to implement something completely different under the scaffolding, to avoid having discussions with the analysts, that checked that the scaffolding itself did not deviate from their designs.

So, my take in this kind of 5th generation (as they were called back then) code generation frameworks is that it encourages the kind of behaviour I saw. And when the same people that do the design also do the programming (the mason architects coders of our time [4]), this way of working is just redundant. Diagrams and models have their place in documenting a project, but certainly not in trying (and failing) to specify everything that can happen in a system.

Wow...I've almost written a blog post xD

-----

[0]: What a shitty place to work in, at every level. No joy was possible in that environment. Sociopaths thrived and naturally floated to the management positions. As we say in Spain: shit always float to the top.

I have so many stories to tell of that place...and I was only 6 months there!

[1]: lowly paid and lowly valued programmer-monkeys, literally the term they used when they thought we couldn't hear it (and for a more colourful spanish variation of it: "picatas" which was a derogative term meaning Typist)...how the tables have turned since then...

[2]: As we all know, it's just a sham. We were never consultancies, just the equivalent of cheap sweatshops for our french overlords, who came to Spain because programmer's salaries and labor rights were lower than in France. Still...they offered better salaries than the native "consultancies", so there's that. A common theme in Spain, actually. At least foreign exploiters treat labor better than our own national exploiters.

The situation has greatly improved since those times, and you can find genuinely good (foreign) companies to work at, in Madrid or Barcelona. The consultancies still exist, but they're no longer 100% of the job market now.

[3]: Because, naturally, the churn was stupidly high at the "picatas" level, who could find better offers and situations just by changing jobs every 6 months, which I did. I remember at that time how they tried to FUD us into "loyalty" by saying that they did not recruit people that had this kind of job-hopping CVs. It was false, of course, they were desperate to find people, so they took what they could. My father said the same to me. I don't doubt that was how it was at his time. That era of employee and employer loyalty had long passed by that time, if it ever really existed from the employer side in the first place (I doubt it, IMO it's just that employees had even less choice and were educated by society into loyalty for your task masters)

[4]: I'm very glad of how the industry has evolved, job-wise. These times are much more interesting from a technical point of view, than what existed in the past. I get enjoyment out of my job now, and that is priceless. Also the high salaries help. Not as high as outside Spain, of course, but high enough for a good life.

Most of the real world distributed systems would have some videos in some conferences: Spanner: https://www.youtube.com/watch?v=IfsTINNCooY

Chubby: https://www.youtube.com/watch?v=PqItueBaiRg

Anything Leslie Lamport: https://www.youtube.com/watch?v=-4Yp3j_jk8Q

https://www.youtube.com/watch?v=kYX6UrY_ooA

Also the Distributed system course at MIT is fantastic. The labs are also great way to get your hands dirty with distributed system. The link to the class schedule is here: https://pdos.csail.mit.edu/6.824/schedule.html

Leslie Lamport thinks the same:

https://dl.acm.org/doi/fullHtml/10.1145/2736348

Even a rough sketch is good enough a lot of the time:

https://m.youtube.com/watch?v=-4Yp3j_jk8Q

Leslie Lamport (of Paxos, LaTeX, and TLA+ fame) has been making this point for years. Basically that in order to design a piece of software, you need to be able to create a spec, and the best way of doing that is through mathematics.

E.g.

- https://lamport.azurewebsites.net/tla/math-knowledge.html

- https://youtu.be/-4Yp3j_jk8Q

⬐ pmiller2

I agree in principle, but there’s a rather fundamental problem here: writing the spec has to be easier than writing the program. Otherwise,we should just write a compiler for the spec language and save ourselves a step, or blunder on by writing the program without a spec, as is usually done.

⬐ AlexCoventry

Writing a useful TLA+ spec will usually be easier than writing an operational program with the functionality the spec describes, because it lets you abstract over the uninteresting parts.

⬐ pmiller2

That seems like it just pushes all the bugs into the “uninteresting” parts.

⬐ AlexCoventry

Not really. Some parts are harder to reason about than others, especially interactions between components of a distributed system.

⬐ hwayne

It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers in two regions."

⬐ anaphor

I think if you're doing your spec as a combination of high level set theory or algebra and some prose, then it should be easier than writing the program itself (assuming you know a bit about math and how to write a spec).

The question is how much time is it worth putting into writing a detailed spec. I think the answer is that it really depends on the size and complexity of your software.

I think the idea is that programmers have to be comfortable with writing something down, even if it's not perfect. A half-baked spec is better than no spec, basically. Otherwise you will likely end up with spaghetti code that needs to be rewritten or scrapped.

⬐ pmiller2

I already write my specs as a combination of math and prose. It’s just that the math portion is empty. /s

Seriously, though, that prose portion is where the vast majority of the bugs will be.

No. Have a look at this video. It's worth it. He's just saying that you should think before you code and that most specifications should be just a few sentences stating what you intend to do. Code as a blueprint is not the same.

https://youtu.be/-4Yp3j_jk8Q

The article is about TDD. You can see on the page, that they are offering a TDD course using ruby/rails. TDD in Ruby community is overhyped. This infection spread to management too. If you apply to Ruby job today, you better have TDD or BDD in your CV. If you don't, you are garbage to them. I have experience with people infected with TDD in ruby land, they often look down on people who don't write tests for every single line of code they write. I am all for unit testing, but can we at least acknowledge that example based testing is just no panacea for bad software.

No, easily testable code does not always imply good design.

People that don't do TDD are actually doing TDD too, they test code in REPL/console/browser/whatever, they just don't save those "tests".

You can not write perfect example based tests, that would cover all possible inputs and states of your system. You need generative testing solutions for this. Let the program write tests for you. [0] [1]

See what Leslie Lamport [2] has to say about TDD --> https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3158s He nearly flips out on the guy :)) Surely Leslie knows what he is talking about.

I am ok with unit testing as a communication/documentation tool, so developers know how to use some piece of library. And to prevent regressions with new releases, but I would argue that you can never completely prevent those anyway, requirements change all the time. Maintenance of a large test suite can quickly get out of hand.

[0] https://wiki.haskell.org/Introduction_to_QuickCheck1

[1] https://clojure.org/about/spec

[2] https://en.wikipedia.org/wiki/Leslie_Lamport

Short answer: try starting with TLA+.

I'm working on this. My colleague, who is mentoring me, is the one who's finishing his PhD in software engineering. It's his guidance that has helped me so I don't have a good answer for how to teach yourself yet. We're working on a project to create specifications for Openstack and are learning a lot by working together on how formal specifications could be taught to hackers and developers with no formal mathematics training, etc.

If you want a brief introduction to the ideas try some of Leslie Lamports talks on TLA+:

https://www.youtube.com/watch?v=iCRqE59VXT0

https://www.youtube.com/watch?v=-4Yp3j_jk8Q

I saw the TLA+ talk [1] recently and was surprised there was no discussion of code-generation.

Once you've spent a significant effort in writing and verifying a formal spec for a program, there should be an automated mapping between it and the implementation, or at least a template of such implementation.

[1]: https://www.youtube.com/watch?v=-4Yp3j_jk8Q

⬐ nickpsecurity

Code generation is a separate issue. Things you can look into are Fowler's old Perfect Developer toolkit, SCADE toolkit, model-driven development in Rockwell-Collins SHADE program, iMatix's DSL's for various things, certified compilers/optimizers for functional languages such as FLINT ML, and CompCert C compiler for low-level correspondence. Also, high-level metaprogramming systems such as Racket give you the ability to transform things in many ways. The automated programming field will have things for you. My scheme was to use a knowledge-based programming approach leveraging a combination of the above work to generate certified code from functional specifications. Haven't built it yet but would make a practical Ph.D.

Hope you find some of the above enjoyable or helpful on your journey to end-to-end, verified software.

⬐ smallape

I can't remember which talk it was, but Lamport said for code generation you should look elsewhere.

⬐ ahelwer

There is a difference between formal specification and formal verification. Formal specification is what we have with TLA+: you create a high-level description of your system, to which you apply software tools to check the design. It's like blueprints for software.

Formal verification deals with proving that the actual code you write implements a formal specification. This is a much, much harder problem. Usually, it involves cajoling a theorem prover by adding lots of annotations to your code. There's been some impressive work with the Ironclad project from MSR[1] which brought this down to ~5 lines of annotation per single line of implementation code - within striking distance of unit testing! Still, probably a decade or more away from widespread use.

Formal verification isn't quite what you meant, though. You were talking about code generation. For general systems specified by TLA+, this isn't going to be useful unless you write in a very idiomatic way; in which case TLA+ is just a very high-level programming language. However, code generation is implemented in some specification languages that deal with very specific areas of system design. I'm thinking primarily of the P language[2], which is used to specify & check state machines and includes code generation capabilities for C++ and C#.

[1] https://www.usenix.org/conference/osdi14/technical-sessions/...

[2] http://research.microsoft.com/apps/pubs/default.aspx?id=1771...

Higher quality version of this same talk (given at a different event): https://www.youtube.com/watch?v=-4Yp3j_jk8Q