1. 3

    Gazing into the abyss of a multi-step test suite and a series of patches that may or may not fix any of the issues that the test suite currently is showing exist.

    I should have scripted this a few days ago, but I didn’t, did I. Oh well.

    1. 3

      Work: Mostly cross-compiling a bunch of tests so I can see how good LLVM is at compiling things for RISC-V. When I know what it cannot do, I’ll go and fix LLVM! I have some other changes to LLVM to work on while waiting for code to build, of course. A colleague has been working on another suite of test cases and has got much further than I have, but he

      Home: Not much. Need to get fully settled into new flat and life in a new city.

      1. 1

        the HoTT book is available online as a free PDF, and also as a print-on-demand book. I have a physical copy, I know quite a few academics (including students) who have the same, though probably they all have the PDF too.

        1. 3

          A friend of mine has this, but I think she’s still learning how to use it: https://twiddler.tekgear.com

          1. 1

            Thanks, I love lobsters for this kind of insights)))

          1. 7

            Nice tricks. I’m still going to encourage a safe language without hacks or big gaps in type system handling more error classes. @tedu, what you think of Cyclone as a C developer? It was designed by academics rather than people in C’s trenches. What do you like and not like about the safer C? I’d say aside from dynamic, memory management which might build on Rust’s or Nim’s models in next iteration.

            1. 6

              I think the problem with cyclone is it requires a fair amount of rewriting. It’s like C, but it’s not C. On the other hand, I really liked CCured. http://www.utdallas.edu/~hamlen/Papers/necula_ccured.pdf

              1. 2

                Yeah, CCured was cool. Necula is also fairly badass in high-assurance security having invented proof-carrying code.

                How far away from “like C, but not C” is acceptable in that case? Especially trying to damage-limit the risky features while still letting you use them where appropriate. I’m guessing you liked CCured since it works better with your legacy code (i.e. no rewriting). I always thought we could take something like that as default, profile it for where performance hit is too high, and then add annotations or restructuring (eg a borrow-checker) to reduce the runtime checks selectively.

                1. 2

                  Yes, drop in compatibility is a requirement. I don’t think ccured is going anywhere at this stage, but in the cases where it can’t prove a bounds and must insert checks, it could also issue warnings such that you can iteratively improve performance.

                  1. 3

                    Do look at Checked C - it’s getting close to a place where “drop-in compatibility” is there, and then it has tools to do CCured-like analyses on the source code (rather than within the compiler), so you can slowly upgrade code from C. Hopefully it’s an answer to “What does CCured/Deputy look like when applied to real code, with 10 years more PL/Static Analysis theory”.

                    1. 1

                      Thanks, I’ll check that out.

              2. 1

                What’s your opinion on the CHERI architecture?

                It seems like a ton of resource overhead to protect against bad code. I brought that up to someone presenting it (I believe he worked on it) and his response was that we’re never going to be rid of insecure buggy code, so better to add more protection at the architecture level. I’m still not sure where I stand on adding more compiler/language checks vs adding more hardware checks.

              1. 7

                They are likely to remove this in the next C standard (or may have already), because a declaration with a static size is “compatible” with a declaration with no static size, and thus you can get unsoundness.

                So your compiler should accept (though the semantics of static suggest this program would be wrong):

                void foo(int a[static 3]);
                void foo(int a[]);

                According to the spec, this is fine, but when you come to define the function foo, should it respect the ‘static’ annotation? The spec doesn’t say, and doing static analysis of subsumption for the expressions after ‘static’ is much more complex to keep sound than C prefers in its specification.

                Update: The issue and proposed fix are detailed in N2074, if you’re interested.

                1. 3

                  I wondered about the zero-overhead assertion. It is not clear that in all (standard-compliant) compilers, on all platforms, this is zero-overhead. Unlike Rust and Haskell, C provides no such guarantees. Nice it works on some platforms though.

                  Anyway, it’s nice that C programmers finally discovered Haskell’s newtype, even if there are a lot of ways around the safety this method provides.

                  1. 1


                  1. 1

                    Re. 1:

                    “[Haskell] code gets obscured by successive by pack and unpack calls”

                    “You can call pack and unpack strings to go back an forth to a List Char representation [in Idris].”

                    So, they’re exactly the same? I’m not sure what the improvement is here. Just the fact that Idris uses the equivalent of Text by default?

                    Some of these other things are very cool. I’m especially a fan of the Show instance of IO values.

                    1. 6

                      There are some functions that are directly : String -> String -> String, concat comes to mind. This makes them much more efficient.

                      1. 4

                        So, they’re exactly the same? I’m not sure what the improvement is here. Just the fact that Idris uses the equivalent of Text by default?

                        Pretty much. It doesn’t care about the details around chars unless you specifically request them.

                        1. 6

                          Which is a big deal, if you ask me. Haskell strings are a horror story because the default implementation is not the sane one. This is also true for more base library objects, such as ListT that was re-implemented several times.

                          Take a look at Python 3. Not many libraries re-implement base functionality. Perhaps because it keeps evolving to actually remain a practical base. Unicode mess was cleaned up, collections were added, asyncio will help unification across several frameworks and so on.

                        2. 1

                          So, they’re exactly the same? I’m not sure what the improvement is here. Just the fact that Idris uses the equivalent of Text by default?

                          Being Text by default means one isn’t likely to call pack and unpack much: all the APIs are in terms of an efficient type so you won’t be converting for efficiency and then deconverting to show (or perform other operations).

                        1. 11

                          We don’t have tags for x86, x64, mips, arm, sparc, blackfin, or any other architectures that actually exist in large numbers.

                          1. 7

                            Exactly. Hardware is sufficient. Especially since most RISC-V projects are vaporware in terms of hardware one can buy. It’s not like people are missing a lot of opportunities.

                            1. 2

                              My personal argument here would be that risc-v is unique in that it is a real royalty-free open standard, where those other architectures given as examples are all either fully proprietary or not both open and royalty free, with the notable exception of sparc. I do, however, understand the counterargument presented here.

                              1. 1

                                I’m not sure royalty free has any bearing on it being specifically unique in its feature set that articles about it will be so different from other architecture articles.

                            1. 11

                              Have you considered LaTeX? If the only reason is that you don’t know it, you should un-not-know yourself immediately.

                              1. 4

                                troff is where its at.

                                1. 2

                                  I had a brief period of trying out troff, but went back to LaTeX mostly because the community is much larger (it’s used by a lot of conferences and journals), and therefore the packages and maintenance are better.

                                  For simple stuff using the built-in styles, I find them mostly a wash in terms of the actual formatting language. Both have their quirks, but I could use either. Troff gets the edge because it’s smaller, and often included in default Unix installs, though not on all Unixes.

                                  But if you’re not doing something very simple, there is a high chance LaTeX will have a package to do what you want, while there is much less chance troff will. That could possibly be overcome if DIYing it in troff were much better than in TeX, but at least for me, it wasn’t. Writing anything custom in LaTeX involves a terrible 70s stack language combined with C-preprocessor-style text-substitution macros, so obviously sucks. But writing anything custom in troff is also really byzantine. My conclusion was that I should treat them both as languages only writeable by wizards, and therefore I prefer TeX mostly because its wizarding community is more active.

                                  1. 1

                                    What resources would you recommend to get started with troff? I have experience writing pages in mdoc format already, so roff syntax isn’t alien to me.

                                  2. 2

                                    I have. Long before I was a programmer, I was a math researcher. None of my papers made it to the outside world but I have an Erdos number of 4. I’ve also used math markup for sites like Quora.

                                    I’ve actually never written a document from scratch in LaTeX, because mathematicians are lazy (that’s a good thing, it’s connected to why many of them are so fucking brilliant) and reuse old document templates, so that’s what everyone told me to do and that’s what I did and it worked. I suppose there’s no good reason not to know, though, especially since I’m going back into research as soon as a few details (well, one detail that takes a very long time) click into place. That’s a big part of why I’ve been living the 8-to-2 life (not a six-hour day, but that other 2 that’s mostly for drunks, poets, and cats) on this novel.

                                    The truth is, and I’ll readily admit this, that I’m also pretty lazy (although perhaps not brilliant, because I’ve gotten into my share of dumb shit). That is, I don’t want to fiddle with details other than the story and prose. That’s why I used Google Docs instead of learning a new platform from scratch. Soon enough, oops, 120k words. How much fiddling I do depends, I imagine, on whether I e-publish or go with a mainstream publisher. This is far and away the best thing that I’ve written, so the support/distribution of a publisher might be the way to go. I have no problem with giving my work away for free (you don’t write fiction to make money; they odds are almost as bad as in tech startups) but you actually reach more of an audience if you’re selling a $25 rectangular prism with art done by someone much more skilled in the visual arts.

                                    When I talk about fiddling and how much I want to avoid it, I’m not talking about grammar or sentence structure or even comma placement because all of that is my job. I’m talking about stuff like “this chapter is 19.1 pages, but 0.1 of a page is bad form so let’s take two lines off each other page”. It’s a hassle and while it does really matter (turning a page is 250-500 msec and can be flow-breaking) it’s not what I’m good at. If it becomes my job because I decide to e-publish, then I need the most powerful tools out there.

                                    1. 9

                                      Well, if you’ve done anything with LaTeX before, I think it would be very easy for you to grab a LaTeX novel template and get going. That’s especially since a novel doesn’t really need any complicated structured content or funky layout.

                                      One of the things I like the most when writing LaTeX is how your brain doesn’t waste cycles on “oh, now this line is on the next page”, or “damn you <WYSWIG_Editor>, I didn’t intend that to be a bullet list”. I think it’s a feature that what you see isn’t what you get, so, while writing a paragraph, you have no excuse to think about anything but the content.

                                      I’ve never published any book, so I don’t know, maybe there are extremely domain-specific tools out there that somehow do very domain specific things that would be very hard to do with LaTeX, but if the alternatives are google docs, MS word, etc., I wouldn’t consider them over LaTeX.

                                      1. 1

                                        Of course LaTeX can be an endless yak-shave, it was written by computer scientists after all.

                                        I know people who swear by the “memoir” package, and that’ll do 90% of the layout stuff that you need, has a few options (and is completely customizable if you want to go down that rabbit hole). It’s aimed at this sort of thing.

                                        If it was a technical book, the MIT press also has released their LaTeX template/class, but that seems less useful in this instance.

                                    1. 5

                                      I’m looking to add some formal methods into my workflow, and it’s a tossup between climbing the Alloy, CoQ, TLA+, or Idris learning curves.

                                      1. 18

                                        I think it really depends on what you want to use it for. Here’s an extremely misleading overview of the use cases:

                                        • Coq: Good for writing mathematical proofs. “Does my proof of the P=NP have any errors?”
                                        • Alloy: Good for topologies and static structures. “Can someone be their own grandchild?”
                                        • TLA+: Good for state machines and concurrent systems. “Can we guarantee all uploaded data will eventually be processed?”
                                        • Idris: The only one of the four that’s an actual programming language.

                                        Personally I’m biased towards TLA+, because that’s the only one I know, but Idris is on my list and I’ve been making bedroom eyes at Alloy.

                                        1. 21

                                          Good except that Coq, although made for mathematical proof, is probably the most widely-used for verifying algorithms for programming problems that are usually then extracted into programming languages like Haskell or Ocaml. Almost all the best work on verified programs, from OS’s to compilers, is done with Coq or HOL. I’m not saying it was ideal choice for that but that’s what they’re using. Lots of stuff to build on, too, like Bedrock, CompCert, and protocol models. On HOL side, AutoCorres, CakeML, and Verdi come to mind.

                                          People should also look into K Framework & Maude for the rewriting/equational logic side of things. Those get too little attention despite how easily many problems are solved in them. Then there’s B method and Event-B with refinement if anyone wants to go all out on turning algorithms or systems into verified code. Gonna be work like Coq or HOL, though, since refinement is always a pain. Finally, Abstract State Machines if you really just want specifications not proofs as they’re easiest to learn and most successful in industry. I’m recommending TLA+ over it as it has more tooling & educational resources now days w/ similar capabilities.

                                          1. 2

                                            Verdi (the distributed systems proof system, including the proof of raft’s safety) was done in Coq. If you mean a different Verdi I apologise in advance.

                                            1. 1

                                              I misremembered it. You’re right. It was security protocols and clocks in HOL. Verdi used Coq.

                                      1. 21

                                        “made illegal” my ass, and any sort of framing like disabled people are party poopers for this sort of thing: get fucked

                                        1. 13

                                          Completely agree, and the people behind this mirroring seemed to miss the point entirely.

                                          The content wasn’t “made illegal”. The illegal part was for a public, tax funded institution to release it without meeting the requirements of ADA. Nobody’s taking down MIT’s OpenCourseWare videos, because they actually followed the law and put captioning on theirs.

                                          It really wouldn’t surprise me if this gets a DMCA take down notice or something like that, because mirroring it really doesn’t change the fact that it came from Berkley without the legally required captions.

                                          1. 3

                                            According to the site, most of it was released under a creative commons license.

                                            1. 2

                                              I’m not sure that matters if it wasn’t legal to release it without captions in the first place.

                                              1. 2

                                                It wasn’t legal for a public institution to release it without captions. CC allows you to re-distribute, maybe getting rid of captions, and i don’t believe there’s an obligation to stay ADA compliant if it’s a private (rather than state) resource.

                                                Now, it would be great to see an effort to get all of these captioned as well, but them not being deleted is a first step towards this.

                                          2. 5

                                            I agree with the sentiment, but maybe be a bit politer than just raging?

                                            1. 1

                                              This is called tone policing.

                                              1. 6

                                                Only if it’s used as criticism or harassment, and I don’t think that’s what angersock meant? I think angersock was just asking for rational discourse.

                                                1. 2

                                                  Rage very much has its place in discourse any the initial post makes it very clear why the are enraged.

                                                  1. 10

                                                    Disagree. Original post was:

                                                    “made illegal” my ass, and any sort of framing like disabled people are party poopers for this sort of thing: get fucked

                                                    This can be paraphrased (slightly) as:

                                                    This makes me angry, and fuck anybody who says the disabled people are being party poopers.

                                                    That’s an opinion and an imperative. There is no “This makes me angry (because of reasons x, y z). There is no "fuck anybody (and here’s what that policy would look like)”.

                                                    It’s a yelp of anger that gets upvotes for the emotion and not the content. There isn’t anything to engage with as it’s just an unsupported opinion, and not a terribly articulate or nuanced one at that.

                                                    This sort of thing is shitposting.

                                            2. 4

                                              I agree. I REALLY don’t understand why Berkeley didn’t think out of box a little and find a way to get these subtitled :\

                                            1. 26

                                              They’re removing the content from iTunes U, YouTube, and their own website because two people (not UC Berkeley students) sued saying the educational content was inaccessible to deaf students (since the video content lacked subtitles and the audio content lacked transcripts).

                                              They’re removing the content rather than go back and go through the expense of adding subtitles and transcripts.

                                              1. 22

                                                Am I the only one who find this lawsuit ridiculous? Yes content should be accessible to everyone, but because it isn’t (likely because it wasn’t at the time it was created) nobody should allowed to see it?

                                                1. 31

                                                  On the one hand, yes, but on the other hand: UC Berkeley is a state school, funded in a large part by taxes; we as a society have decided that our public institutions have a commitment to be accessible. Moreover, they take huge amounts of federal grants. They’ve been aware of the ADA since its inception and have committed to following it, and even more than that they should have known. Every single other piece of educational media they produce is made accessible so it’s not like they didn’t have the resources to do it or knowledge that it needed to be done.

                                                  So the law being what it is, should we say “well, obviously you knew what the law was, but you didn’t follow it this time, but we’ll give you a pass because…?”

                                                  1. 17

                                                    I don’t find the lawsuit ridiculous, but I do find the ruling/outcome ridiculous. There are so many better solutions to this problem than simply removing the content. They could use mturk or undergrads to do the transcriptions, or crowsource the transcriptions by adding a feature to their website, and so on. Removing the content is a net loss for everyone, whereas keeping them up while building a system to transcribe them over time is a net gain, even if the transcriptions take a long time to complete.

                                                    1. 29

                                                      That was Berkeley’s choice. The judge didn’t tell them to take them down, but to make them accessible. Rather than do that, Berkeley chose to remove them.

                                                      1. 4

                                                        Thanks for all the above explanation, I haven’t seen the details of the lawsuit. IMO Berkeley made a poor choice, and LBRY is right for wanting to archive this content.

                                                        According to this calculator, running 20,000 hours through the Google Speech API would cost about $28k. Even if the actual cost is twice that much, you would think Berkeley would be able to afford it.

                                                        1. 18

                                                          In this specific case, the courts already explicitly found the automatic transcript insufficiently accurate to meet the obligations of ADA.

                                                          1. 3

                                                            At the risk of sending this even more off topic, here is an alternative argument that points to a possible technical solution: Accessibility isn’t free, and we need freedom to make things accessible. The irony is that Berkeley’s actions as a result of the lawsuit could end up stalling advances in accessibility technology.

                                                            1. 1

                                                              Reading comments, I don’t remember anyone mentioning that they were in a budget crisis of some sort per those comments. A college doing cuts across the board is well within reason able to terminate 20,000 videos that (a) resulted in legal fees, (b) will cost them tons of money to fix, and © not producing revenue. It’s a loss of money they need for their own students. I still find it non-optimal solution given the public benefit of those vids if other cuts are made.

                                                              People in comments section are talking about all kinds of groups fighting over budget. This decision is part of a larger picture of budget cuts. And the lawsuit inspiring it came from freeloaders who weren’t even students at their university. That just had to be irritating to admins trying to decide what’s worth their money for their students. It would increase the odds of them giving the middle finger to whoever sued them on top of the budget issues.

                                                    2. 10

                                                      UC Berkeley does follow the ADA and provides captioned media for their own students. What happened at my university (and presumably at Berkeley) was that at the start of the semester, any students which needed closed captioning, or other support told the disabilities office which courses they were taking, and they coordinated with the course to get the videos closed captioned, student notes photocopied, e.t.c.

                                                      The law was written for a time when no-one had anticipated a university making their course content freely available to anyone in the entire world.

                                                      1. 8

                                                        we as a society have decided that our public institutions have a commitment to be accessible.

                                                        And if it is not accessible in the euphemistic sense, it should not be accessible period.

                                                        Let’s make our society more equal by cutting off the legs of anybody that’s too tall.

                                                        1. 1

                                                          I’d be more sympathetic if it weren’t for the fact that they’re a publicly-funded institution. If anything should be accessible, it should be things paid for with taxes. Berkeley made the wrong decision to take the videos down, but that wasn’t ordered by the judge: they had the option to make them accessible, they just didn’t. Letting them stay up would be to say that they could flout the law with impunity as long as it was “for the right reasons”.

                                                          (Now I’d be fine with amending the law to carve out exceptions, but the law as it exists today is what it is.)

                                                        2. 3

                                                          Not only “they should have known”, but indeed they did, concretely, know. Quoting from the DoJ Letter:

                                                          Beginning July 1, 2015, UC Berkeley advised the Department that all faculty using the self-service model will be asked to sign off on a list of accessibility resource reviews prior to publishing the course.

                                                          The materials that didn’t go through the “self-service” model were distributed using the “Berkeley Resource Center for Online Education [which] follows best practices in design for accessibility” and presumably were fine. It was all the self-service publishing of materials between 2012-2015 where Berkeley wasn’t properly monitoring things.

                                                        3. 4

                                                          The lawsuit was perfectly reasonable. Berkeley is ridiculous, for being told “you must make your content accessible” and deciding the best path forward was to delete it all.

                                                          1. 15

                                                            I dont know. My impression is this is a bonus freebie they’re giving away to people not paying their University plus their students. Going through all that video to subtitle it could cost a lot of money. All for content not bringing them any money.

                                                            I wonder what the labor cost would’ve been to them given people doing subs sould have to watch the videos probably paid by the hour. Some administrator estimated the number & decided freeloaders arent worth it. I think they’re wrong but I see the reasoning.

                                                            1. 5

                                                              They’re a public university, everything they do is paid for by taxes, so the concept of “this is a freebie” doesn’t apply. The state still paid someone to film them, someone to edit them, someone to upload them, someone to build the website.

                                                              Why should they get to skip the last steps of “someone to caption them” and “someone to make sure disabled people can use the website”?

                                                              Related point: Maybe if everyone committed to getting videos captioned/made accessible, there would be more accessibility experts, and the price of doing so would come down.

                                                              1. 1

                                                                The University’s funding is mixed. They probably shouldn’t have skipped the last step. The takedown due to budgeting issues or politics is still a net loss. Fortunately, it got cancelled out by people restoring access to the videos.

                                                                Your last idea is interesting where that could happen. Im not hopeful because it’s mostly a labor-intensive process. Constantly listening, transcribing, or fixing.

                                                              2. 4

                                                                this is what happens when a public institution for knowledge is treated as a profit driven enterprise. of course it doesn’t bring them in any money. they should be optimizing for knowledge generation and dissemination, not money.

                                                                yes, it takes money to generate and disseminate information. that’s what the public funds (and tuition) are for.

                                                                (this comment not specifically aimed at you, nickpsecurity [shout out – love your posts], but just a reaction to reading your comment “all for content not bringing them money”)

                                                                1. 3

                                                                  Appreciate your clarification at the end. :) Well, institutions like this get complex. The successful ones are run much like businesses out of necessity. Those that don’t remain low impact or sometimes disappear in the case of research labs. The business-like style is also how they get as much money as they do for their operations. That probably influences the culture of their administrators. There might also be an ego component given it’s a prestigious institution reacting to a lawsuit trying to force a course of action. Many groups give the middle finger as a reflex if it’s possible.

                                                                  I agree the organizations should optimize for knowledge generation and dissemination. It’s why I said “I think they’re wrong.” Subtitling it would be justifiable expense for social impact. It might even get paid back some if the courses lead H.S. students to choose their university. The businessmen looking out for university’s self-interest thought otherwise. Fortunately, it all got copied and reposted anyway. :)

                                                          1. 8

                                                            I’ve spent some time learning a bit of Idris for fun. To set expectations, if you do learn it, learn it for fun not for profit. I don’t mean that it’s a small, new language, but rather that the cool features it has I have struggled a bit to find great uses for them. Maybe it just takes a big mind shift, I don’t know. To compare, a type system that Haskell or Ocaml or SML has, has much clearer wins for my day-to-day life. I want to use these languages at work and argue for it. The type system of Idris on the other hand has powerful features but I haven’t really figured out how to apply them to the use-cases I have. But, that means when I use it, it’s purely for the joy of doing so, and that is its own reward.

                                                            As for the book, I don’t know, but I’ll probably grab it to hopefully help with what I said above.

                                                            1. 6

                                                              the cool features it has I have struggled a bit to find great uses for them. Maybe it just takes a big mind shift

                                                              There are plenty of good uses for dependent types. Here’s what I believe to be an important example. We generally want parallelism in our language to be deterministic. Nondeterminism leads to annoying heisenbugs, security concerns via side channel attacks, and can also break language guarantees like referential transparency or type safety. There are a number of approaches to ensuring determinacy, such as Determinator (which modifies the OS communication primitives), CoreDet (which modifies the scheduler), or DPJ, which uses a type and effect system.

                                                              More recently there is LVish which allows threads to communicate only with data types that form a lattice. This is an expressive approach but it is difficult to extend with new data types, because we must trust the programmer that what they provided indeed forms a lattice. With dependent types you can enforce these properties through the type system.

                                                              That being said, adding dependent types to a language involves a lot of tradeoffs that I think are simply unacceptable for general purpose programming. Recursion must be limited if you want the types to mean anything (and in the parallel example we do), type inference is weakened, and writing proof terms is a huge pain in the ass. I don’t think dependent types are useful enough to make these tradeoffs, and would rather use them in a special purpose language like Coq.

                                                              1. 3

                                                                Yeah… I tried to learn it for fun and got stuck. I intend to go back.

                                                                On my most recent try, somehow I wound up doing a “fun, easy, simple” project for which I needed to implement row types. Which I don’t even understand in any other language either.

                                                                I advise learning it with simpler things first. :)

                                                                1. 3

                                                                  I’ll first say I don’t do functional programming or formal work. Ive read on a ton of it to track capabilities of field. I also read debates by veterans on places like Lambda the Ultimate. The point they all say of it is verification of properties of your programs instead of say productivity like some language features. Dependeng types supposedly are easier than theorem provers to do this.

                                                                  The arguments by each side boiled down to one of two positions: (a) general purpose languages with dependent types are easier to point it might increase adoption of formal-like methods; (b) verifying serious programs and properties with dependent types is about as hard as other methods like Coq so might as well avoid them in favor of stuff like Coq.

                                                                  My barely-informed opinion leans toward the latter as both ATS and Idris code + proofs of anything complex looks like as much gibberish to me as similar stuff I see in Coq papers. The guides had a lot of similar material in them, too. So, I was leaning on it being better just to learn the real stuff.

                                                                  If you do want to learn dependent types, Chlipala has a book on it and has done lots of useful verifications.



                                                                  Far as what cmm is saying, Brady et al have a nice paper on checking resource use:


                                                                  1. 7

                                                                    (a) general purpose languages with dependent types are easier to point it might increase adoption of formal-like methods; (b) verifying serious programs and properties with dependent types is about as hard as other methods like Coq so might as well avoid them in favor of stuff like Coq.

                                                                    Coq isn’t a different method than Dependent types, it’s a different underlying formalisation to Idris', but they are both dependently-typed programming languages, and proving something in Idris produces something exactly the same as proving something in Coq.

                                                                    They do, however, differ in two main ways.

                                                                    1. Coq is a lot more mature, and expects proofs to proceed in a certain way, using tactics. Idris' libraries are considerably less mature, and its proof system has recently changed quite a lot, but there is nothing theoretically holding Idris back from completing the same proofs Coq can. (Please someone correct me if I am wrong)
                                                                    2. Coq will never claim to be general-purpose. In Coq you can never write a function which coq believes to be partial (non-terminating/non-productive), whereas in idris, this restriction is relaxed. This allows for more algorithms to be written in Idris, even although you may not be able to prove to the type checker that they are terminating/productive. Edwin is really pushing for Idris to be practical and general-purpose, so that you can ignore the dependently-typed parts if you want.
                                                                    1. 7

                                                                      I’ve not used Idris in anger but I have used ATS. I find having the ability to prove things in the language itself more useful than using an external system like Coq. When debugging an ATS program I’ll often start with adding dependent types and some proofs to narrow things down. These then stay within the program and the additional checks ensure safety if anyone changes it in the future. With an external checker like Coq I could write proofs in that, translate to my actual language but then if people make changes they must know to re-check assumptions in Coq. Maybe they will, probably they won’t.

                                                                      I’d say it’s just as useful to learn the capabilities within ATS and Idris to learn how such things help in development of production code and then followup with Coq, etc to get a deeper dive in systems that are oriented solely around proofs and dependant types. You can then apply what you learn there to the programs being written in ATS, Idris, etc.

                                                                      One could turn your argument around that “Real World” applications Coq tend to be full of complex stuff that looks like nothing to do with the application being written. Might as well program in ATS or Idris where you can have your program structured like you’d write code normally and add the complex gibberish looking stuff later as needed.

                                                                      That said, if you learn Coq first, or ATS or Idris first, it doesn’t really matter - it’s still an interesting field to learn and whatever one gets you interested enough to stick with it is really what matters.

                                                                  2. 7

                                                                    Yes, I think it’s a great book. Not only is it a good resource for learning Idris but it also goes through how to interactively write programs guided by types and the Idris REPL.

                                                                    This approach to development reminds me of “Programming in the Debugger” approaches used in Smalltalk and Self. In those languages you define a function but leave parts unimplemented, When you run and test it the debugger will appear for the unimplemented portions. You then implement that functionality while in the debugger and resume the program execution where it was. In this way you interactively build your program while it runs.

                                                                    An approach demonstrated in the book for Idris is to define your types and let the compiler help you interactively build the implementation as it typechecks. You can leave ‘holes’ in your program that the type checker identifies and helps you determine what should go in there. You can also leave ‘holes’ in your type definitions and be guided towards what the correct types should be. For this alone I found the book worth reading.

                                                                    This book has good coverage of dependant types for programming with Idris and a useful resources for practical examples of dependent type usage. The authors writing style is clear and easy to follow with lots of examples.

                                                                    1. 6

                                                                      I can’t view Twitter where I am. But I’m a huge fan of Idris' design and I think he’s the language author? Which doesn’t always lead to the best language books, but one can hope; in any case this is probably the first proper Idris book.

                                                                      1. 3

                                                                        Yes, Edwin Brady is the author of Idris itself, and this is the first book on Idris (though there have been books on dependent types before).

                                                                    1. 5

                                                                      Here are a few from literature I like:

                                                                      End-To-End Arguments in System Design - all about correct placement of functionality where it can be of most use.

                                                                      Why Do Computers Stop and What Can Be Done About It


                                                                      On Understanding Types, Data Abstraction, and Polymorphism answering the important question “what do we mean by ‘type’?”.

                                                                      1. 1

                                                                        I like this sentence from the abstract of your last suggestion:

                                                                        We christen this language Fun because ‘fun’ instead of λ is the functional abstraction keyword and because it is pleasant to deal with.

                                                                      1. 4

                                                                        Reason : OCaml :: CoffeeScript : JavaScript ? But, from a quick glance at the syntax changes, it doesn’t seem to add much but some “simplicity”. Maybe that’s a good thing, but OCaml, and it’s syntax is already incredibly simple by many regards…

                                                                        1. 3

                                                                          it adds consistency more than simplicity. i’m not sure why the change from -> to => (not really a fan of that, on trivial aesthetic grounds), but everything else fixes definite warts in the existing syntax.

                                                                          1. 4

                                                                            isn’t -> a type-level operator? I think for clarity issues it makes sense to split type-level operators -> and expression-level operators => so they are definitively separate.

                                                                            Haskell’s [a] being both an expression and a type was something that tripped me up early, the same kind-of applies to (a,b) being both an expression and a type.

                                                                            Now, on the other hand, I like Idris, where there are a whole lot of these things that are type-level or expression-level which have the same syntax because they are the same thing. This is neat and super useful :D

                                                                            1. 1

                                                                              they’ve been unifying syntax elsewhere - e.g.

                                                                              type person = {name: string, age: int};
                                                                              let somePerson = {name: "Guy", age: 30};
                                                                              let {name: n, age: a} = somePerson;
                                                                              1. 1


                                                                        1. 4

                                                                          This page might be useful for those of you who already know OCaml: Reason and OCaml: A quick reference for OCaml Programmers

                                                                          1. 3

                                                                            I’m not an OCaml programmer, so much as a motivated dabbler, but I can’t find much to object to in the Reason syntax changes.

                                                                            1. 9

                                                                              Most of them are quite nice. Re-appropriating = for mutable field changes instead of equality is pretty stupid, and replacing match with switch is silly, but whatever. Overall the greater consistency is a win; I remember being very frustrated with OCaml trying to guess where I needed to keep spamming more parens to get the parser to understand what I meant.

                                                                              1. 2

                                                                                OCaml already has a second syntax aimed at ironning out the kinks in the original - the so-called “revised syntax”. http://caml.inria.fr/pub/docs/manual-camlp4/manual007.html

                                                                                The general consensus seems to be that while revised syntax is a little better, having two different syntaxes isn’t worth the gains. Seems like this fragmentation will be similar.

                                                                                That being said, ML would be a great language choice for many programmers/tasks. I’m thrilled to see it in wider use.

                                                                            1. 1

                                                                              Concepts Techniques and Models of Computer Programming. Gearing up for grad school in September, I read half of this last summer, going to finish it because I hate unfinished books.

                                                                              Non-tech books? Just read skyfaring, which I liked but others have found pretentious. Loved Turing’s Cathedral by Dyson, and Down to the sea in ships by Horatio Clare was also great. Last fiction book I read was Station Eleven, also recommended. :D

                                                                              1. 6

                                                                                Today I:

                                                                                • brought in dead sheep (and dead sheep’s smell)
                                                                                • mowed a field because it was full of weeds
                                                                                • wrote most of a submission for ICFP SRC (more of my undergrad work)

                                                                                Tomorrow: meetings in town.

                                                                                Rest of week: reading, ‘riting, not much 'rithmetic. Def some farm stuff too.

                                                                                1. 5

                                                                                  I think publishing lists like this is fantastic. :D

                                                                                  1. 3

                                                                                    Agreed! These focus largely on memory safety, which is an important concern, but it’s pretty important for anyone designing a language to think in these terms in a whole lot of domains. It’s a lot easier to recognize one’s own ideas as bad when comparing them to someone else’s.