[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Choose and TLC

I haven't shopped for a computer recently, but I expect it's hard to find one with a processor chip that doesn't have at least 4 cores.  In a few years it will be hard to find one with fewer than 16 cores.  Every programmer in industry who is building the kind of large distributed system that requires TLA+ specifications should have access to a server farm with dozens or even hundreds of machines--e.g., by buying time on Azure or Amazon's cloud.  I want TLA+ to be useful for people who don't have much computing power--in part, because I want TLA+ to be taught at universities.  But ultimately, TLA+ will be successful only if it's used in industry.

I should also have mentioned that I believe that the most important area of TLC evaluation that needs improvement is its error reporting.  Speeding up evaluation saves computer time.  Speeding up finding the cause of an error saves human time.