User loginNavigation |
LtU ForumBitC is back
I didn't really look at BitC till the project went dormant. Now I have, I think it's great. Every language should have a BitC-like implementation layer. determining subsumption of regular languagesI recently came across the concept of regular expression types, such as in XDuce. The idea seems promising, but the current implementations all seem excessively restrictive (disallowing nontrivial patterns), so I was wondering about the feasibility of further development in this area. The bottleneck for regular types would definitely be in trying to determine subsumption of these types in an automated manner, but I can't seem to find much literature on the subject. Computationally how hard is it to determine equivalence/subsumption of regular languages in general. Finite? Hard? Easy? For at least some languages (a+ <: a*) this sort of comparison seems plausible. If this comparison isn't plausible in general, is there any way to foresee which languages are easy to compare/hard to compare? On the (Alleged) Value of Proof for AssuranceEhud is about to be annoyed with me. :-) I am lately suffering from doubts about whether the value of proof is justfied by its cost. Some questions, in no particular order:
There is no question in my mind that proof processes generate more robust code. Yet the general concensus seems to be that this robustness is much more an emergent consequence of rigorously understanding the problem then a result of the proof discharge. In this view, the primary benefit of proof (in the context of assurance) is largely to keep the specification "honest". If this is in fact the goal, is proof the best way to accomplish that goal? How much of that goal can be undertaken by type systems? In a private conversation, Gernot Heiser (NICTA, OK Labs) was recently asked how use of proof impacted their QA costs. As I recall it, his answer was that they run between 1.5x and 2x the end-to-end cost of conventional development and testing, but they achieve much higher confidence. My questions:
In a second private conversation, Eric Rudder observed that one of the costs of proof-based methodology was a loss of ability to rapidly adapt software to new requirements and new demands. It follows that proof is not always appropriate, and that a more continuous cost/time/benefit option space would be desirable. My own observation is that in the end, systems need to be robust, and they include components that lie well outside our ability to prove them. In many cases, type can be usefully exploited when proof cannot, and there is a training cost to educating people in both domains. So finally my question: Once we step away from formal semantics and PL insights (which are certainly good things), what is the proper role of proof in real-world production? And what is the proper role of advanced type systems? Type system design choicesHi LtU, I'm working on the design of a programming language (as I'm sure many of you are). And sometimes I feel the need to brainstorm about a new idea. LtU looks exactly like the kind of community I want to reach. My experience with different programming languages is limited (I'm basically a C++ guy) and I want to learn. The LtU forum is not meant for design discussions, but I've been allowed to post a link to another discussion group. If you would like to respond, please do it there, not here. Any thoughts would be most appreciated! [ANN] Code Generation 2010 program availableThe program for this year's Code Generation conference is now available at: http://www.codegeneration.net/cg2010/programme.php The conference, now in its fourth year, is Europe's leading event on Model-Driven Software Development. Highlights include: - keynotes from (Pragmatic) Dave Thomas and Eelco Visser (Delft University of Technology) - Language Extension with MPS: Markus Völter (independent/itemis AG) / Konstantin Solomatov (JetBrains, s.r.o.) - Proven best practices for successful MDD adoption: Steven Kelly & Juha-Pekka Tolvanen (MetaCase) An early-bird booking period runs until 1st April with up to 20% off booking fees. Full-time academics can also claim a further 20% discount. The event takes place 16-18 June 2010 in Cambridge, UK. Visit http://www.codegeneration.net/cg2010/ for more information. By Mark Dalgarno at 2010-03-13 19:35 | LtU Forum | login or register to post comments | other blogs | 516 reads
Urbit: Functional programming from scratchC. Guy Yarvin recently published an interesting new project in language/systems design. It includes a simple formal model of computation called Nock ("comparable to the lambda calculus, but meant as foundational system software rather than foundational metamathematics") and a self-hosted language called Watt that compiles to Nock. The motivation? To provide a fully-specified foundation for Urbit, a hypothetical system architecture that uses content-centric networking to distribute code and data in a functional global namespace. Yarvin's own descriptions are rather lengthy, so I tried to provide a shorter introduction here. Interesting questions for LtU readers: Nock formulas are terribly inefficient for real computation (for example, decrement(n) is an O(n) operation). Yarvin intends to make Watt efficient by writing fast implementations (in C, say) for standard "kernel" functions like decrement, add, multiply, and more. He calls these fast native implementations "jets." So how one can trust that jets are equivalent to the functional Nock/Watt code that they replace? Yarvin has proposed the classic n-version software engineering trick of comparing both implementations with the same inputs, but in addition the classic problems with that approach, there is the additional hurdle that the pure Nock code might be so inefficient that it is impractical to run it on most inputs. Is the goal of a minimal pure standard compromised by the need to implement a common set of "impure" jets too? Should let be generalized?I came across this paper proposing that Let Should Not Be Generalized (TLDI 2010, Vytiniotis, Peyton Jones, and Schrijvers).
I'm actually fairly convinced by this. Among other things, it provides a fairly clear path to eliminating the monomorphism restriction:
Are they right? Are they wrong? Has anyone laid out the case for the defense? A Wiki for LaTeX (LaTiKi)I am pleased to announce that LaTiKi is now available as a public beta. LaTiKi accepts LaTeX syntax as input rather than the wiki syntax that is I have prepared a sandbox wiki with some of Philip Wadler's papers on the If any readers are interested in this project and would like to do a similar By Stuart Beard at 2010-03-10 08:10 | LtU Forum | login or register to post comments | other blogs | 758 reads
Have tracing JIT compilers won?I've been watching the interpreter and JIT compiler competitions a bit in the JavaScript and Lua worlds. I haven't collected much organized data but the impression I'm getting is that tracing JIT's are turning up as the winners: sometimes even beating programs statically compiled with GCC. Is there a growing body of evidence that tracing JIT compilers are the horse to bet on? Will a more static style JIT like Google's V8 be able to keep up? Thanks, [I promoted this item to the front page, since the discussion is highly interesting & informative. -- Ehud] Fighting Bit Rot with Types (Scala Collections)didn't see it mentioned yet. i would excerpt the abstract were it not for the fact that the pdf is horribly broken such that no spaces are copied-and-pasted. yay usability. the gist: statically typed collections library ends up with duplication, ironically? and new advances let it be excitingly refactored to make everybody happy again. i think that is interesting because i do believe static typing has some gotchyas. |
Browse archivesActive forum topics |