14 ms·
“What next?”
- leeoniya 9y agoit's interesting that Rust isn't mentioned once in his post. i wonder if he's disheartened with the direction his baby went.
- drdre2001 9y agoWhat direction would that be?
- leeoniya 9y agoi can't find the previous hn submission, but i think he wrote a post about how much it has changed since its inception. early Rust was quite different - not as low-level, had a GC, green threads, other stuff. some info here: https://news.ycombinator.com/item?id=13533701 https://news.ycombinator.com/item?id=13533701
- tomjakubowski 9y agoPeople often speculate about this, which boggles me since graydon remarks positively on the current state of Rust all the time. http://graydon2.dreamwidth.org/247406.html http://graydon2.dreamwidth.org/247406.html https://twitter.com/graydon_pub/status/886212237987368960 https://twitter.com/graydon_pub/status/886212237987368960 He even addresses the changes to the runtime: https://twitter.com/graydon_pub/status/705226109856526336 https://twitter.com/graydon_pub/status/705226109856526336
- ben0x539 9y agoNot sure if comparing Rust's relevance to that of the gopher protocol is really a positive remark. ;)
- adwhit 9y agoJust to add (written just after 1.0): http://graydon2.dreamwidth.org/214016.html http://graydon2.dreamwidth.org/214016.html I think the above post indicates that he is extremely proud of how Rust turned out.
- bjz_ 9y agoThe question he is answering is: "After memory safety, what do you think is the next big step for compiled languages to take?" It might be that he thinks it has successfully pushed the state of the art in terms of regions and affine type systems, but that there are still things outside that to explore and push. 'Parametric mutability' seems to be at least in part a response to some patterns that have emerged in Rust due to the lack of this feature.
- carussell 9y agoAll this and handling overflow still doesn't make the list. Had it been the case that easy considerations for overflow were baked into C back then, we probably wouldn't be dealing with hardware where handling overflow is even more difficult than it would have been on the PDP-11. (On the PDP-11, overflow would have trapped.) At the very least, it would be the norm for compilers to emulate it whether there was efficient machine-level support or not. However, that didn't happen, and because of that, even Rust finds it acceptable to punt on overflow for performance reasons.
- Animats 9y agoOn the PDP-11, overflow would have trapped. On the DEC VAX, overflow could be set to trap, based on a bit mask at the beginning of each function, but that was not the case on the PDP-11. Nobody used that feature. I once modified the C compiler for the VAX to make integer overflow trap, and rebuilt standard utilities. Most of them trapped on integer overflow. If you want arithmetic to wrap, you should have to write something like n := (n + 1) mod (2^32); Let the optimizer figure out there's a cheap way to do that.
- deleted 9y ago[deleted]
- legulere 9y agoAs a clarification, I guess you are speaking about integer overflows. Your comment confused me a bit as I thought that you speak about buffer overflows at first.
- naasking 9y ago> All this and handling overflow still doesn't make the list. Because it's either a solved problem if you just use infinite precision numbers, or it's encompassed by other things the article lists, like refinement types/extended static checking and errors.
- VHRanger 9y agoDesigning a "checkedInt" class is not trivial
- AstralStorm 9y agoExtra credit for whoever implements logic proofs on concurrent applications.
- manmal 9y agoI believe that this will not happen until we have a general AI capable of doing this. (And it will rewrite its own code first :))
- pron 9y agoLanguages designed for safety-critical realtime applications do just that. Well, they don't use proofs as proofs generally have a bad cost/benefit ratio (even for sequential programs), but they do use temporal logics that easily deal with concurrency, which they then verify mostly automatically. Temporal logics were introduced to CS in the late '70s, have resulted in at least two Turing awards, and have enjoyed some success in industry.
- mcguire 9y agoDo you have links? I'm aware of TLA+ and (Jay Misra's) Unity (https://en.wikipedia.org/wiki/UNITY_(programming_language) https://en.wikipedia.org/wiki/UNITY_(programming_language)), but I haven't seen any other uses of temporal logics. (The lengths people will go to in order to get away from box and diamond...)
- pron 9y agoTake a look at Esterel[1], and its current incarnation, SCADE[2], which is used for avionics. [1]: https://en.wikipedia.org/wiki/Esterel https://en.wikipedia.org/wiki/Esterel [2]: http://www.esterel-technologies.com/products/scade-suite/ http://www.esterel-technologies.com/products/scade-suite/
- mhhf 9y agohave a look on CLF[1] and Meta-CLF2[2]: [1] http://www.sciencedirect.com/science/article/pii/S1571066108000790 http://www.sciencedirect.com/science/article/pii/S1571066108... [2] https://www.cs.cmu.edu/~iliano/projects/metaCLF2/index.shtml https://www.cs.cmu.edu/~iliano/projects/metaCLF2/index.shtml
- hderms 9y agoFantastic article. This is the kind of stuff I go to Hacker News to read. Had never even heard of half of these conceptual leaps.
- gavanwoolery 9y agoI like to read about various problems in language design, as someone who is relatively naive to its deeper intricacies it really helps broaden my view. That said I have seen a trend towards adding various bells and whistles to languages without any sort of consideration as to whether it actually, in a measurable way, makes the language better. The downside to adding an additional feature is that you are much more likely to introduce leaky abstraction (even things as minor as syntactical sugar). Your language has more "gotchas", a steeper learning curve, and a higher chance of getting things wrong or not understanding what is going on under the hood. For this reason, I have always appreciated relatively simple homoiconic languages that are close-to-the-metal. That said, the universe of tools and build systems around these languages has been a growing pile of cruft and garbage for quite some time, for understandable reasons. I envision the sweet spot lies at a super-simple system language with a tightly-knit and extensible metaprogramming layer on top of it, and a consistent method of accessing common hardware and I/O. Instant recompilation ("scripting") seamlessly tied to highly optimized compilation would be ideal while I am making a wishlist :)
- ColanR 9y agoEver heard of K?
- imnotlost 9y agoSpecial K? It'll take care of most of your language problems, computer or otherwise.
- kbenson 9y agoIs there a free version? I was interested I was interested in learning it a few years ago but couldn't find a version that was free for both commercial and non-commercial use, which tempered my enthusiasm.
- grayrest 9y agoTo my knowledge, there isn't a full OSS implementation of K/Q. I do know of a K5 interpreter in JS [1] but otherwise I've only been able to find the free for personal use 32 bit Q distribution. [1] https://github.com/JohnEarnest/ok https://github.com/JohnEarnest/ok
- ilaksh 9y agoI think at some point we will get to projection editors being mainstream for programming, and eventually things that we normally consider user activities will be recognized as programming when they involve Turing complete configurability. This will be an offshoot of more projection editing. I also think that eventually we may see a truly common semantic definitional layer that programming languages and operating systems can be built off of. It's just like the types of metastructures used as the basis for many platforms today, but with the idea of creating a truly Uber platform. Another futuristic idea I had would be a VR projectional programming system where components would be plugged and configured in 3d. Another idea might be to find a way to take the flexibility of advanced neural networks and make it a core feature of a programming language.
- msangi 9y agoIt's interesting that he doesn't want to draw too much attention to actors while they are prominent in Chris Lattner's manifesto for Swift [1] [1] https://gist.github.com/lattner/31ed37682ef1576b16bca1432ea9f782 https://gist.github.com/lattner/31ed37682ef1576b16bca1432ea9...
- mcguire 9y agoActors are a bit of a off-the-wall paradigm (https://patterns.ponylang.org/async/actorpromise.html https://patterns.ponylang.org/async/actorpromise.html), and I'm (as an old network protocol guy) not sure I'm happy with the attempts to make message passing look like sequential programming (like async/await). I kinda see where Graydon is coming from. I have this broken half-assed Pony parser combinator thing staring at me right now.
- ehnto 9y agoI know I am basically dangeling meat into lions den with this question; How has PHP7 done in regards to the Modules section or modularity he speaks of? I am interested in genuine and objective replies of course. (Yes your joke is probably very funny and I am sure it's a novel and exciting quip about the state of affairs in 2006 when wordpress was the flagship product)
- kbenson 9y agoThere's probably an interesting discussion to be had about the merits of shipping fast with a few killer features and taking your time layer in comparison to well thought out initial features. PHP is probably a great language now. I used it in the PHP 4 and 5 days. Coming from Perl, that was particularly painful.
- tel 9y agoHaven't used PHP in more than a decade so I looked up the documentation. The most relevant parts I could find were "Classes and Objects" and "Namespaces". After a rough review, I'd say that the it is possible that PHP inner classes provide one of the most rudimentary components of "type theoretic modules" in a partial and likely broken way. I don't mean this as a diss at PHP—it's just hard to do it right. Namespaces also provide something similar to "type theoretic modules" but they provide only the very most prosaic, simple, and unimportant function: namely, namespacing.
- thaumasiotes 9y ago> the state of affairs in 2006 when wordpress was the flagship product Does PHP have a different flagship product now?
- goldenkey 9y agoCake and dont forget Wikipedia.
- TazeTSchnitzel 9y agoIt doesn't. WordPress is still the elephant (heh, elePHPant…) in the room. PHP has other significant projects built on it of course, but WordPress is a behemoth nothing can hope to beat.
- statictype 9y agoSo Graydon works at Apple on Swift? Wasn't he the original designer of Rust and employed at Mozilla? Surprised that this move completely went under my radar
- steveklabnik 9y agoThat's how he likes it, to be honest. He doesn't want it to be some statement about Rust or Swift; he left Rust long ago, did some other stuff for a while, and there's only so many "work on a programming language" jobs out there. In general the Rust and Swift teams are very friendly with one another, and have shared several devs.
- statictype 9y agoSure. He was very impressively neutral and rational about Monotone as well.
- platz 9y agowhats wrong with software transactional memory?
- poopoopoopoo 9y agoSTM in Haskell is a thing of beauty
- qznc 9y agoNobody figured out how to implement it efficiently yet.
- marcosdumay 9y agoHaskell's STM is not efficient?
- platz 9y agoInstead of opt-in STM, perhaps he's referring to whole-program STM like when they tried to do that in C#.
- qznc 9y agoHaskell is not efficient with all these thunks and memory allocations. Maybe the way Haskell does STM is efficient relatively. However, you cannot port that to C/C++/Java/C#, because they do not provide the type system to make it safe. Maybe Rust can deliver. A quick search gives me rust-stm [0]. All these disclaimers in the README looks discouraging, though. For example, "Calls to atomically should not be nested", but isn't that the whole point about composable STM? Repeating transactions is a no-go, because it does not mix well with side effects. Thus, we need a lock-everything-required scheme. You do not want to expose this in the type system, because it explodes everywhere and gets really tiresome. Thus you need a whole-world analysis to find out what is "required" for a transaction. That breaks modular compilation and is inconvenient in general. In general, I don't see how this could work even a very high level. [0] https://github.com/Marthog/rust-stm https://github.com/Marthog/rust-stm
- fulafel 9y agoAgain my pet ignored language/compiler technology issue goes unmentioned: data layout optimizations. Control flow and computation optimizations have enabled use of higher level abstractions with little or no performance penalty, but at the same time it's almost unheard of to automatically perform (or even facilitate) the data structure transformations that are daily bread and butter for programmers doing performance work. Things like AoS->SoA conversion, compressed object references, shrinking fields based on range analysis, flattening/dernormalizing data that is used together, converting cold struct members to indirect lookups, compiling different versions of the code for different call sites based on input data, etc. It's baffling considering that everyone agrees memory access and cache footprint are the current primary perf bottlenecks, to the point that experts recommend considering on-die computation is free and counting only memory accesses in first-order performance approximations.
- cmrx64 9y agohttp://llvm.org/pubs/ http://llvm.org/pubs/ Ctrl+F for "data structure". It's actually the reason LLVM exists at all: http://llvm.org/pubs/2002-06-AutomaticPoolAllocation.html http://llvm.org/pubs/2002-06-AutomaticPoolAllocation.html http://llvm.org/pubs/2003-04-29-DataStructureAnalysisTR.html http://llvm.org/pubs/2003-04-29-DataStructureAnalysisTR.html http://cgo.org/cgo2004/papers/06_76_lattner_c.pdf http://cgo.org/cgo2004/papers/06_76_lattner_c.pdf
- fulafel 9y agoYes, there's a little research about it out there, but the industry side seems to be in deeper apathy about it. It would be very interesting to hear what happened to these LLVM research directions. I guess the default answer is "nobody wanted to fund it after the publications got written"...
- nostrademons 9y agoIt might just be timing. 2004 was when everyone was switching from Java and C++ to Perl, PHP, Python, and Ruby. Hard to make a case for a compiler optimization that might save 10x on a couple percent of workloads when everybody a.) is focused on the workloads that it's not useful for and b.) is using languages that give up 30x performance from the beginning. Things may be different now that Moore's Law no longer holds and many programs are cache-bound, but any current research also needs to take into account GPUs, distributed computing, and deep learning. There might be room for new research, but the research would likely be as much about auto-vectorization and minimizing trips between memory spaces as about local optimizations like AoS -> SoA conversion.
- jez 9y agoGrayson's very first answer to "what's next" is "ML modules," a language feature probably few people have experienced first hand. We're talking about ML-style modules here, which are quite precisely defined alongside a language (as opposed to a "module" as more commonly exists in a language, which is just a heap of somewhat related identifiers). ML modules can be found in the mainstream ML family languages (Standard ML, Ocaml) as well as some lesser known languages (1ML, Manticore, RAML, and many more). It's really hard to do justice explaining how amazing modules are. They capture the essence of abstraction incredibly well, giving you plenty of expressive power (alongside an equally powerful type system). Importantly, they compose; you can write functions from modules to modules! (This is even more impressive than you think: modules have runtime (dynamic) AND compile time (static) components. You've certainly written functions on runtime values before, and you may have even written functions on static types before. But have you written one function that operates on both a static and a dynamic thing at the same time? And what kind of power does this give you? Basically, creating abstractions is effortless.) To learn more, I recommend you read Danny Gratzer's "A Crash Course on ML Modules"[1]. It's a good jumping off point. From there, try your hand at learning SML or Ocaml and tinker. ML modules are great! [1]: https://jozefg.bitbucket.io/posts/2015-01-08-modules.html https://jozefg.bitbucket.io/posts/2015-01-08-modules.html
- cmrx64 9y ago1ML just shows that advanced (first-class) ML modules are really just System F_omega. That's just barely more than Haskell! More languages need to expose it nicely. But we already have most if not all the technology we need to make them efficient and worthwhile, vs just possible. This isn't a research problem. This is a design/HCI problem.
- iso-8859-1 9y agoDo you think Backpack solved that problem for Haskell?
- mcguire 9y agohttps://news.ycombinator.com/item?id=15053706 https://news.ycombinator.com/item?id=15053706
- Animats 9y agoOne big problem we're now backing into is having incompatible paradigms in the same language. Pure callback, like Javascript, is fine. Pure threading with locks is fine. But having async/await and blocking locks in the same program gets painful fast and leads to deadlocks. Especially if both systems don't understand each other's locking. (Go tries to get this right, with unified locking; Python doesn't.) The same is true of functional programming. Pure functional is fine. Pure imperative is fine. Both in the same language get complicated. (Rust may have overdone it here.) More elaborate type systems may not be helpful. We've been there in other contexts, with SOAP-type RPC and XML schemas, superseded by the more casual JSON. Mechanisms for attaching software unit A to software unit B usually involve one being the master defining the interface and the other being the slave written to the interface. If A calls B and A defines the interface, A is a "framework". If B defines the interface, B is a "library" or "API". We don't know how to do this symmetrically, other than by much manually written glue code. Doing user-defined work at compile time is still not going well. Generics and templates keep growing in complexity. Making templates Turing-complete didn't help.
- mpweiher 9y ago> incompatible paradigms See Architectural Mismatch or, Why it's hard to build systems out of existing parts[1] Yes, we are not good at it, but we need to do it. Very often, the dominant paradigm is not appropriate for the application at hand, and often no single paradigm is appropriate for the entire application. For example, UI programming does not really fit call/return well at all[2]. > attaching software unit A to software unit B .. master/slave Case in point: this is largely due to the call/return architectural style being so incredibly dominant that we don't even see it as a distinct style, with alternatives. I am calling it 'The Gentle Tyranny of Call/Return'. [1] http://www.cs.cmu.edu/afs/cs.cmu.edu/project/able/www/paper_abstracts/archmismatch-icse17.html http://www.cs.cmu.edu/afs/cs.cmu.edu/project/able/www/paper_... [2] http://dl.ifip.org/db/conf/ehci/ehci2007/Chatty07.pdf http://dl.ifip.org/db/conf/ehci/ehci2007/Chatty07.pdf
- Animats 9y agoSee Architectural Mismatch or, Why it's hard to build systems out of existing parts If you want to study that, look at ROS, the Robot Operating System. ROS is a piece of middleware for interprocess communication on Linux, plus a huge collection of existing robotics, image processing, and machine learning tools which have been hammered into using that middleware. The dents show. There's so much dependency and version pinning that just installing it without breaking a Ubuntu distribution is tough. It does sort of work, and it's used by many academic projects. In a more general sense, we don't have a good handle on "big objects". Examples of "big objects" are a spreadsheet embedded in a word processor document or a SSL/TLS system. Big objects have things of their own to do and may have internal threads of their own. We don't even have a good name for these. Microsoft has Object Linking and Embedding and the Common Object Model, which date from the early 1990s and live on in .NET and the newer Windows Runtime. These are usually implemented, somewhat painfully, through the DLL mechanism, shared memory, and through inter-process communication. All this is somewhat alien to the Unix/Linux world, which never really had things like that except as emulations of what Microsoft did. "Big object" concepts barely exist at the language level. Maybe they should.
- rtpg 9y agoThe blurring of types and values as part of the static checking very much speaks to me. I've been using Typescript a lot recently with union types, guards, and other tools. It's clear to me that the type system is very complex and powerful! But sometimes I would like to make assertions that are hard to express in the limited syntax of types. Haskell has similar issues when trying to do type-level programming. Having ways to generate types dynamically and hook into typechecking to check properties more deeply would be super useful for a lot of web tools like ORMs.
- charlieflowers 9y agoI believe F# is rich in features like this. I am only an F# outsider who has read about such features, but check out F# type providers.
- mcguire 9y agoCheck Idris (https://www.idris-lang.org/ https://www.idris-lang.org/) and if you have a chance, work through the Idris book, Type Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...).
- bjz_ 9y agoI would love to see some advancements into distributed, statically typed languages that can be run on across cluster, and that would support type-safe, rolling deployments. One would have to ensure that state could be migrated safely, and that messaging can still happen between the nodes of different versions. Similar to thinking about this 'temporal' dimension of code, it would be cool to see us push versioning and library upgrades further, perhaps supporting automatic migrations.
- doublec 9y agoHave you seen Alice ML? It's a Standard ML variant that includes serialization of types and support for distributed programming. [1] http://www.ps.uni-saarland.de/alice/manual/tour.html#distribution http://www.ps.uni-saarland.de/alice/manual/tour.html#distrib...
- bjz_ 9y agoHow does it handle heterogeneous clusters that might have different versions of code running? Or is it like Cloud Haskell where you have to bring everything down when deploying?
- imtringued 9y agoI would start a bit simpler. Are there any statically typed serialisation formats like flatbuffers or cap'n proto where you can statically verify that version 1.0 and version 1.2 are compatible but version 1.2 and 2.0 are not?
- kentonv 9y agoNot sure if I completely understand the question, but... Protobuf, Cap'n Proto, Flatbuffers, and anything else with a similar design gives you the ability to verify that two versions of the protocol are "compatible" insofar as: - If a new version of the program reads a message from an older version which is missing some newly-added field, that field will assigned a default value or "null", but the rest of the message will parse fine. - If an old version of the program reads a message from a newer version which has some new fields that the old version doesn't know about, it will ignore those fields, but can parse the rest of the message just fine. Of course, just because you've verified that the fields line up doesn't prove that the old and new versions of the program are actually compatible. The interpretation of the protocol could change in an incompatible way without any change to the protocol itself. Verifying compatibility at that level is an AI-complete problem. But in practice, it works very well. Enabling safe incremental, rolling updates of components in a distributed system is exactly what Protobuf was designed to do and has been doing for >15 years at Google.
- baby 9y agoCan someone edit the title to something clearer? Thanks!
- rurban 9y agoNo type system improvements to support concurrency safety?
- iso-8859-1 9y agoI think dependent types is next big step, and it also blurs the line between compilation and runtime. This will enable applications to do domain specific optimizations since types become so much more expressive. Purity allows for automatic parallelization. What Edward Kmett does in C++ here: https://www.youtube.com/watch?v=KzqNQMpRbac https://www.youtube.com/watch?v=KzqNQMpRbac could be the default for all computation. On a modern computer, data parallelism is free, since SIMD instructions take just as long as any other instruction.
- jancsika 9y agoI'm surprised build time wasn't on the list. Curious and can't find anything: what's the most complex golang program out there, and how long does it take to compile?
- pebers 9y agojujud is commonly used as a benchmark for the Go compiler / linker due to being probably the biggest open source project. Can't find the actual compile times right now though, only relative figures.
- borplk 9y agoI'd say the elephant in the room is graduating beyond plaintext (projectional editor, model-based editor). If you think about it so many of our problems are a direct result of representing software as a bunch of files and folders with plaintext. Our "fancy" editors and "intellisense" only goes so far. Language evolution is slowed down because syntax is fragile and parsing is hard. A "software as data model" approach takes a lot of that away. You can cut down so much boilerplate and noise because you can have certain behaviours and attributes of the software be hidden from immediate view or condensed down into a colour or an icon. Plaintext forces you to have a visually distracting element in front of you for every little thing. So as a result you end up with obscure characters and generally noisy code. If your software is always in a rich data model format your editor can show you different views of it depending on the context. So how you view your software when you are in "debug mode" could be wildly different from how you view it in "documentation mode" or "development mode". You can also pull things from arbitrarily places into a single view at will. Thinking of software as "bunch of files stored in folders" comes with a lot baggage and a lot of assumptions. It inherently biases how you organise things. And it forces you to do things that are not always in your interest. For example you may be "forced" to break things into smaller pieces more than you would like because things get visually too distracting or the file gets too big. All of that stuff are arbitrary side effects of this ancient view of software that will immediately go away as soon as you treat AND ALWAYS KEEP your software as a rich data model. Hell all of the problems with parsing text and ambiguity in sytnax and so on will also disappear.
- di4na 9y agoThat is totally true and it expands the programming possibilities... But... it make debugging harder without even more tooling. And debugging is most of the time spent in software... which probably explain the origin of the problem. Especially when you need to reverse engineer code provided by a vendor.
- jerf 9y agoBroadly speaking, I agree with beagle3's point (probably above this comment). But the thing that keeps me from being willing to quite commit to it is that it is generally a bit unfair to expect someone to produce this alternative programming paradigm and immediately be better than the previous one, which may or may not be broken or better or worse but has certainly had five or six orders of magnitude more time poured into it. If it's truly the "silver bullet" I'd still say I expect to see some evidence of that in some domain relatively quickly, because it is supposed to be the silver bullet after all. But it would take time to discover that.
- simonebrunozzi 9y agoI would have preferred a more informative HN title, instead of a semi-clickbaity "What next?", e.g. "The next big step for compiled languages?"
- tedunangst 9y agoNot everyone writes exclusively for the HN audience.
- ekiru 9y agoI think this is more of a complaint about HN's title policies.
- mcguire 9y ago"Writing this makes me think it deserves a footnote / warning: if while reading these remarks, you feel that modules -- or anything else I'm going to mention here -- are a "simple thing" that's easy to get right, with obvious right answers, I'm going to suggest you're likely suffering some mixture of Stockholm syndrome induced by your current favourite language, Engineer syndrome, and/or Dunning–Kruger effect. Literally thousands of extremely skilled people have spent their lives banging their heads against these problems, and every shipping system has Serious Issues they simply don't deal with right." Amen!
- mcguire 9y ago[Aside: Why do I have the Whiley (http://whiley.org/about/overview/ http://whiley.org/about/overview/) link marked seen?] I was mildly curious why Graydon didn't mention my current, mildly passionate affair, Pony (https://www.ponylang.org/ https://www.ponylang.org/), and its use of capabilities (and actors, and per-actor garbage collection, etc.). Then, I saw, "I had some extended notes here about "less-mainstream paradigms" and/or "things I wouldn't even recommend pursuing", but on reflection, I think it's kinda a bummer to draw too much attention to them. So I'll just leave it at a short list: actors, software transactional memory, lazy evaluation, backtracking, memoizing, "graphical" and/or two-dimensional languages, and user-extensible syntax." Which is mildly upsetting, given that Graydon is one of my spirit animals for programming languages. On the other hand, his bit on ESC/dependent typing/verification tech. covers all my bases: "If you want to play in this space, you ought to study at least Sage, Stardust, Whiley, Frama-C, SPARK-2014, Dafny, F∗, ATS, Xanadu, Idris, Zombie-Trellys, Dependent Haskell, and Liquid Haskell." So I'm mostly as happy as a pig in a blanket. (Specifically, take a look at Dafny (https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny) (probably the poster child for the verification approach) and Idris (https://www.idris-lang.org/ https://www.idris-lang.org/) (voted most likely to be generally usable of the dependently typed languages).
- DonbunEf7 9y agoIndeed, I would say that capability-safety is the next plateau after memory-safety, but most languages are only barely glimpsing the capability horizon.
- jerf 9y agoThis is personally one of my major pet peeves, because I like to write secure code, and I think you very rapidly end up half-reconstructing capabilities work if you do, and it is not hard to notice that you basically get no help whatsoever from languages. It is still clearly a nearly-invisible problem to the vast majority of developers. You need something almost Haskell class simply to assert "Please, at least provide me some evidence that you ran some sort of permission check." to access a resource.
- lazyant 9y agoWhat would be a good book / website to learn the concepts & nomenclature in order to understand the advanced language discussions in HN like this one?
- pas 9y agoI doubt there is one true book for this. For type systems your best bet is to learn languages with advanced typing features. Start with the friendly ones (TypeScript, python mypy, Rust, Haskell) and look at Idris for dependent types. And then reread this post, and ask a lot of questions (reddit, stackexchange, quora).
- hyperpape 9y agoI can't attest to either, having not read them, but you might try Bob Harper's "Practical Foundations for Programming Languages", or Benjamin Pierce "Types and Programming Languages".
- EvilTerran 9y agoI can vouch for TaPL - I can see it on my bookshelf from here. It's a great overview of the foundational concepts in PLT; Pierce's style is remarkable, he writes the most readable academic text I've ever seen. (I also own & admire his Basic Category Theory for Computer Scientists; I'm yet to brave his Advanced Topics in TaPL - I'm sure it's very good, but the contents list intimidates me.)
- ehudla 9y agoThe LtU getting started thread[1] may be worth checking out. [1] http://lambda-the-ultimate.org/node/492 http://lambda-the-ultimate.org/node/492
- dom96 9y agoInteresting to see the mention of effect systems. However, I am disappointed that the Nim programming language wasn't mentioned. Perhaps Eff and Koka have effect systems that are far more extensive, but as a language that doesn't make effect systems its primary feature I think Nim stands out. Here is some more info about Nim's effect system: https://nim-lang.org/docs/manual.html#effect-system https://nim-lang.org/docs/manual.html#effect-system
- deleted 9y ago[deleted]
- ehudla 9y agoLtU thread: http://lambda-the-ultimate.org/node/5466 http://lambda-the-ultimate.org/node/5466
- touisteur 9y agoAbout units and dimensionality, AdaCore tried something in Ada with GNAT : http://www.adacore.com/adaanswers/gems/gem-136-how-tall-is-a-kilogram/ http://www.adacore.com/adaanswers/gems/gem-136-how-tall-is-a... and http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/Physical_units_with_GNAT_GPL_2013-AUJ35.1.pdf http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimens...