Just a consideration: Do these differences in salaries for professors of the different subjects also show up in tuition fees for students of the respective subject?
oh. I always had trouble imagining a mainstream use case for cryptocurrency. Apparently, the use case that it'll finally find is providing infrastructure for negative interest rates set by central banks.
s/click/viewers and the basic business model has been going strong for half a century.
s/clicks/listeners and the basic business model has been going strong for just a little over a century.
s/clicks/circulation and the basic business model has been going strong for at least a few centuries now.
So, never. Or, more accurately, in about 20 years when "clicking" becomes an anachronism and someone will make this comment except it'll be: "s/taps/clicks and this has been going on for half a century"
Mass circulation media date to the early 19th century, so approaching 200 years. Benjamin Day's Sun wasn't the first "penny-press" newspaper, but it transformed the concept, in 1833.
Developments (and cost reductions) in printing and paper-making, as well as rapidly increasing literacy rates, climbing from 25% or lower around 1700 to 90%+ by 1900 throughout much of Europe and North America, also meant that prior to 1800 there really wasn't a mass-circulation media of any stripe, outside religious mass, and that there very much was one afterwards.
Though yes, your observation that this has been going on for a while is valid.
I think this is true of non-writers in general. Writing good fiction is enormously difficult work and reading it is leisure. Creates some tension.
Maybe the same reason we know have people poo-pooing the modern computer age -- moore's law for decades, the modern software stack, the internet, etc. -- as not amazing innovation. And down playing the role all of that has played in everything else humans now do from satellite systems to sequencing the genome. They think that because their interactions with computers are mostly mindless that modern computing must have been no great feat to build.
Because the article is interesting and insightful.
The full paragraph you quote starts with:
"In this article, I try to explain in detail where Frank Herbert got his names, concepts, and words from."
I'm not sure that "but you didn't read the whole book/series!" qualifies as a reasonable critique of someone who's just giving some (AFAICT straight-forward) etymological background on a few names and concepts...
Also, HN is not some high arbiter of taste. It's just a voting-based algorithm, and the population of voters isn't that large. A re-statement of your question might be: "so why did 60 random internet people click on this at around the same time?", and the answer might be "because there were 60 people who like dune, happened to be on hn around the time this was posted, and don't know much about islam/arabic" :)
> ...$25k in loans to make hundreds of thousands more over their life time.
1. Future reward should be discounted, usually by a fairly large constant, because of interest and risk. Also, in many fields, most of those extra hundreds will come toward the end of a career. So, highly discounted.
2. I wonder if it's really a good idea to set up a society where banks that provide educational loans are able to capture huge percentages of future productivity. Seems like this would have all sorts of really negative outcomes. Some of those negative outcomes are already happening -- e.g., we effectively import 90+% of our scientific human capital because US students aren't willing to do phds.
We realize that allowing financiers to capture a big chunk of the rewards for K-12 ed is a bad idea. Why don't we realize that the same is true for college?
1. Enough of the extra income is weighted towards the beginning that for most people it's worth $25k particularly since repayment us based on income.
2. Public loans are over 90% of disbursements, and if you're only borrowing $25k you're definitely getting public loans. Public loans are made directly from the treasury. No banks involved.
Also most stem phds work as researchers and teachers--they generally aren't paying tuition.
> Enough of the extra income is weighted towards the beginning... No banks involved....
Whether it's banks or other taxpayers or recipients of other entitlement programs is, I guess, a bit of a red herring wrt the point I was trying to make.
The question is about the knock-on effects of squeezing an entire generation for some chunk of what they're worth before they even enter the job market.
Again, I think the K-12 analogy is the best way of communicating the point I'm trying to make. Why don't we also charge high school students $10K @ 4% instead of paying for high school through taxes? Well, because that would be a huge net negative for society.
> Also most stem phds work as researchers and teachers--they generally aren't paying tuition.
I have a stem phd :). I was referring to the huge opportunity cost re: delayed earnings. US students opting out of phds because they have huge student debt to service is a real thing. This is true even when the phd would undoubtedly increase lifetime earnings (e.g., students from no-name schools turning down CMU/MIT/Berkeley/Standford phd acceptance letters for mid five figure salaries).
You don't need to pay public loans back while getting a phd, so it's not because they have to service them. An extra few years of interest isn't going to matter in the long run.
If it would undoubtedly increase life time earnings it's a stupid decision to turn it down because of undergrad student loans. That makes absolutely no sense.
>red herring
I was taking your post at face value. It lamented allowing financiers to capture value.
I'm also not against tax payer funded college. But the loan system we have in the US combined with income based repayment is not as bad as people think it is. Mostly people just don't understand income based repayment and public vs. private loans.
There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem.
Is it really true that TLA scales to large programs? Why isn't there a Compcert in TLA? Why isn't there a Flyspec in TLA? And how about stuff like CertiGrad, where just the spec is pretty involved?
My impression has always been that Coq/HOL scale and TLA-style systems break down once your spec gets big enough (let alone the impl).
> There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem.
The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all.
And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how).
> Is it really true that TLA scales to large programs?
Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties.
> Why isn't there a Compcert in TLA?
There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting).
In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try.
Thanks, that's clarifying. You can do this sort of "lightweight" verification in basically any theorem prover. The difference you observe sounds like a difference in community emphasis rather than capability?
There is one big difference in tooling: Coq doesn't have a good model checker. While you can verify several thousand lines of code/spec, writing proofs for those could take months or years, while model-checking is pretty much pushing a button (and then letting the computer or cluster work, possibly for hours or even days), and you probably need to do this a few times, but the difference between having a model checker and not is often the difference between practically reasonable and not. TLA+ has a proof assistant, but people who use TLA+ in industry hardly ever use it because the small added confidence is simply not worth so much more work.
TLA+ does have things that make it hard for you to modularize and reuse pieces of it in the large.
The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all.
The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance. In TLA+'s case, it is easy to add additional new states into a state machine defined in another module (this is TLA+'s celebrated idea of stuttering), but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module (e.g. you have a transaction primitive that allows you to assume that two states can be done simultaneously).
This is complicated by the fact that the easiest verification technique in TLA+ is model-checking, which fares the worst when dealing with transitive chains of logical implication. TLA+'s model checker does not have a native notion of logical implication. Instead the way you e.g. prove the statement A => B is by effectively proving A and B but privileging A to be the search space that the model checker operates in. This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying. You either prove each step with separate models along the chain and just let a human infer that this means A => D, or you prove the statement A => (B and C and D), without using any of the intermediate implications.
Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance.
To some extent this is a limitation inherent in model checking and goes away with the proof based verifier for TLA+ TLAPS. But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers.
I suspect again this is due to both the lack of a package manager in the TLA+ ecosystem as well as some not so ergonomic parts of TLAPS. TLAPS feels very magical. Its main way of proving things is what's often referred to as sledgehammer or auto in other theorem provers; write the next step in your proof and hope the computer is smart enough to infer it from the previous step. It feels magical when it works. When the computer can't figure something out, it can be a huge pain to figure out why. It doesn't feel like I'm mechanically building up a proof so much as it feels like I'm playing a guessing game with the computer to see which leaps of logic it'll accept. This gets better with time as you develop an intuition of which leaps work and which don't, but can still be painful. This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers.
Finally set theory and first order logic, the theoretical basis of TLA+, sometimes makes showing equivalence between items (which is vitally necessary when dealing with code written by multiple individuals who might use different encodings for the same idea) very difficult. In particular, trying to use the fact that A is equivalent to B, therefore some predicate P has an exactly analogous P' on B is tricky. Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up.
All that being said, among the technologies commonly referred to as "formal verification," I would say that TLA+ is the one I would most commonly recommend to people in business situations. This precisely because of what many people view as a flaw, that TLA+ is a formal specification language and not a way to actually write or verify actual running code.
Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices.
Indeed TLA+'s closest competitor on most teams is also precisely what most teams lack, which is high-quality documentation.
This means you can integrate TLA+ into your work with extremely little risk. Try formalizing your mental model in TLA+. See if it reveals interesting conclusions. If it does, congratulations! TLA+ has been useful to you and you can keep it around as an artifact detailing your thoughts in the future. If not, delete your specs and no harm no foul. No code depends on its existence. You don't need some lengthy transition period to migrate systems away from "using" TLA+. You lose no more time than the amount you put into writing your spec.
> The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all.
I currently see this as the biggest barrier to widespread adoption. Not the only barrier, but the biggest by far. A modernized CLI + exportable traces would make a huge difference.
> you to modularize and reuse pieces of it in the large.
There is no such thing as formal specifications "in the large." The largest software specification ever written in any language that could be fully verified is no more than a few thousand lines (although proofs can be very long). Having said that, I think TLA+ module system is fine; reminds me of ML.
> The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance.
I don't think so, but if you're modularizing your specs you may be doing something wrong.
> but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module
Right, but the problem here is fundamental. Verifying temporal quantifiers is co-NP-hard in the number of states.
> This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying.
Yes, but still about 10x less annoying than writing proofs. :)
> Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance.
Again, using composition is a hint that you may be doing it wrong.
> But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers.
Deductive proofs are currently not a viable verification approach in industry (except in some small niches, and/or to tie together model-checking results), so libraries of that kind are mostly useful for researchers who research formal mathematics or deductive verification; that's not exactly TLA+'s target audience. Other proof assistants are used almost exclusively for research or by researchers so they're optimized for that.
> This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers.
That's not why (you can choose specific Isabelle tactics in your BY clause). The reason is that the TLA+ proof language was designed to be declarative. I guess some people prefer a more imperative style.
> Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up.
There are many things in TLA+'s design that make deductive verification harder, and many things in other language's designs that makes deductive verification harder. There is no one best way to do this.
I think the difference is that TLA+ was designed not for research but for industry use, and so its preferences take into account what's feasible. There is no point making something that few people would do easier at the expense of making something many would do harder.
> Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices.
... And because there is no tool in existence that can verify those systems at the code-level anyway, so it's not like there's any other option. You get ~2000-5000 lines of formal spec. You can use them for code and get a tiny program or for a high-level spec formally "divorced" from your code.
There is formal specification in the large if you count formal mathematics. Mizar's library of formalized mathematics is easily millions of lines if not tens of millions of lines at this point. There are individual formalized mathematics repositories in other languages (Coq and Agda included I think? It's been a while since I looked into that) that run into the hundreds of thousands of lines of code.
So there are pointers as to how to organize formal specs for extremely large projects.
The reason as far as I can tell for why there aren't large software verification projects as opposed to pure formal math is that the cost benefit analysis is wildly out of whack. It makes essentially no business sense to try to formally verify things past several thousand lines. This doesn't seem like a bright line to me though, e.g. that there is a technological inflection point at several thousand lines that prevents further scaling. Again formal mathematics repositories are a counterexample. It's just that because of the high cost of formal verification, there is a business ceiling at the equivalent of man hours willing to be spent somewhere in the vicinity of hundreds of thousands of lines of unverified code to millions of lines of unverified code and you can rapidly exhaust that budget with full formal verification (which can easily account for orders of magnitude increases in time spent).
Ah thanks for the TLAPS repo. I forgot about the library, but even there I'm not seeing a lot of reuse in it. There's some of it, but not a lot. Maybe just because users of TLAPS are far fewer than users of TLC.
Indeed you can choose specific Isabelle tactics in your BY line. In practice I'm not sure I've ever seen it in any TLAPS proof. I've very very briefly played with that functionality and at first glance it seems much more difficult than using Isabelle directly because of the added layer of indirection. If you have one in the wild, I'd love to take a look to learn from.
I definitely agree there is no one way to do things. I've left out all the things that I think TLA+ is fantastic at. I think it's the closest thing to mathematics that can be practically used in industry. Far more so than the rhetoric you usually hear about FP languages, TLA+ is immediately familiar to anyone with a pure mathematics background, both syntactically and semantically. TLA+, unlike something like Agda, also has a fairly straightforward set of semantics and mathematical grounding in its theory. The benefit of writing each spec from scratch allows them to be independently understandable with no need to understand the idiosyncrasies of arcane libraries or frameworks.
But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space (which honestly don't bother me, my TLA+ specs are often exponential or worse wrt model checking time in the size of my constants, but I still get a lot of mileage out of them), but rather the difficulty in even expressing that idea. When I'm confronted with wanting one state to stand in for two I often have to resort to using two separate specs, one with fewer states and then the other being the original spec and then showing my new spec fulfills both. I think the modularity problems mostly stemming from tooling and language choices, but a little bit from theory (although Mizar is also set theory based). For example I don't think I've ever used a 3rd party module in a TLA+ spec I've written. Even trying to express the equivalence between two specs that just use different strings for the same states can be tricky. Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems? Or any other specs someone has written specifying one part of their system? That would be pretty awesome if there was something akin to an NPM repository of all these specs for various algos that you could import into your own spec. The tools for this exist in Mizar. They do not for TLA+.
Turning my attention back to deductive verification rather than the expression part of the equation, more specifically for TLAPS, I'm actually not a fan of the imperative tactics that are found in Coq. But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS. Something where you can mix YOLOing with more hands-on proof building, with tactics, functions, or even just a trace of the constraint search would be great.
I think the idea that you have some limited thousands of line to "spend" is a useful bit of intuition. One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.
For example absence of crashing/abnormal exits is something that is feasible to prove on very large codebases. It's hard to do completely end-to-end (even CompCert's front-end isn't proven), mainly because of the difficulty of fully modeling stuff like filesystems, but can be done for modules spanning hundreds of thousands of lines of code. It is of course a weak property. That the program does something is nowhere near the same thing as doing the correct thing. But it is nonetheless a very useful one.
Absence of SQL injection attacks and CSRF attacks are other examples (can be done either by external analysis or by leveraging language level features), although those feel a bit more like cheating since you basically cleverly restrict the amount of code that "matters."
That would be the closest to an alternative to formal specifications I could suggest. I still think formal specs are lower risk because this still requires coding in certain styles amenable to this static check (or languages that enforce it).
> There is formal specification in the large if you count formal mathematics.
Sure, but TLA+ is not aimed at research. The biggest problem, by far, plaguing not just proof assistants but formal logic in general, pretty much since its inception, is complexity. Which is ironic because the entire purpose of formal logic -- from Leibniz's original dream to Frege's early success -- is to be simple, clear and easy tool for practitioners. Compared to the dismal failure of formal logic in achieving that (which was acknowledged and lamented by the likes of von Neumann and Turing, but has since been shrugged off even though the problem has gotten considerably worse), I think the fact that people who are not trained logicians use TLA+ to do real work makes it a crowning achievement not only in software verification but in the history of formal logic. To achieve that, TLA+ had to shed away everything that isn't absolutely necessary. Lamport once said after hearing a lecture about some proposed addition to TLA+: "it's taken you 6 months to add something to TLA+ that it had taken me 15 years to remove".
> It makes essentially no business sense to try to formally verify things past several thousand lines.
Well, we don't know how to do that in a way that would be feasible; I consider that a "limit" because the software we use and need is very commonly three orders of magnitude ahead of what deductive verification can handle. And the gap has been constant or even growing for the past 40 years or so.
> Again formal mathematics repositories are a counterexample.
I disagree. Formal mathematics is about taking years to prove a proposition that could be written in one or a couple of lines. I think that the resemblance between deductive mathematical proofs and deductive software verification is like that between painting the Sistine Chapel and painting a large hospital. The similarity is superficial.
> If you have one in the wild, I'd love to take a look to learn from.
> But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space ... but rather the difficulty in even expressing that idea.
Can you DM me on Twitter (get there from the about page of my blog: https://pron.github.io) or send me an email (my name at Google's mail service)? I'm curious to see the problem you're referring to.
> Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems?
Well, I don't yet understand the exact issue you're having, but no, I don't think that would be particularly helpful at all, for the following reason: If people wanted to modify Paxos itself, they can get their hands on Lamport's spec and tinker with it. If they want to use it as a component, then they can write an abstraction of it in a few line. All of TLA+ is about the abstraction/refinement relation (that is, IMO, what makes its theory cooler than Coq et al. for software).
> But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS.
Yep.
> One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.
Right, but we know more than to say it's just richness. We know exactly what kind of properties scale (through abstract interpretation, of which both type systems and static analysis are examples): inductive (= compositional) ones. I.e. a property such that if it holds for any state (whether or not reachable by the program), then any step in the program preserves it, or, alternatively, a property P, such that P(x) and P(y), where x and y are terms, implies that P(x ∘ y). Problem is that most functional correctness properties are not inductive/compositional for the language (i.e. that the above two description hold for any term in the language).
> That would be the closest to an alternative to formal specifications I could suggest.
I think that's one additional tool. But a knob that's easier to turn is soundness. The difference between verifying a property to 100% certainty and to 99.999% certainty can be 10x in cost, and as -- unlike mathematics -- an engineer is not interested in the correctness of an abstract algorithm but in that of a physical system that can always fail with some nonzero probability -- absolute confidence is never strictly a requirement. Of course, this is not just my opinion but it also seems to be that of many formal methods researchers, which is why concolic testing is such a hot topic right now.
I think that specification and verification must be separate -- i.e. you specify at any "depth" and then choose a verification strategy based on cost/benefit (so, no to dependent types), and in most cases, it's possible that concolic testing would be enough.
1. The very large Coq/Agda texts are usually large because of the proofs, not the specification/propositions. There's a 5-10x ratio, if not more.
2. I don't think that TLA+'s theory is intrinsically more "straightforward" than Agda's, even though it's certainly more familiar (I know some people who would insist that type theory is more straightforward than set theory). I think that a lot of work has gone into making TLA+ relatively easy to grasp; I think it's more design than a specific choice of theory, although the choice of theory certainly affects the design. In addition, as I've already mentioned, I think that TLA itself (i.e. not the set theory in the "+") is a particularly beautiful theory for talking about computation and discrete systems, that has some obvious advantages over the lambda calculus; in particular the abstraction/refinement relation that's the core of TLA (the semantic domain of TLA is a Boolean lattice where the less-than relation is behavior refinement).
This sounds like a problem in your community: a large group of people every year trying, probably often failing, to find concrete ways to actually help out.
Go out and interview folks running non-profits, research labs, churches, health clinics, legal clinics, schools, anyone else who fits into your colleges definition of "community around us".
From those interviews, build a large list of project-sized problem/solution statments for future groups of students. Include skills needed, points of contact, possible adoption challenges, etc. Validate those project descriptions with the people you interview.
Identifying and describing problems that need to be solved and what it means to solve them is something lots of people build careers around
Most luxury apartment buildings have an affiliated cleaning service and can recommend an interior designer.
Find one with a restaurant on the bottom floor and you're done.
It'll cost close to 5K/mo all in for decent square footage. That's before food, which will probably run around 50/day at least. Still very achievable on a dev salary in a major market, as long as you don't make any other expensive life decisions (i.e., children). Not what I would spend my money on, but certainly an option if it's what you want
But, yeah, the delta between econ/law and CS faculty salaries is why I turned down TT offers and went to industry.
They can pay. They're choosing not to.