Omega - Language of the Future
lambda-the-ultimate.org
lambda-the-ultimate.org
http://code.google.com/p/omega/source/browse/#svn/trunk/test...
As a matter of finesse, I think that the correctness vs productivity argument is a specious one when it comes to language design. If correctness is a business requirement then providing language support is a productivity booster for the team (when you consider the timelines of the verification process as part of the development time.) you alluded to different problem domains perhaps requiring formal proof, I just want to suggest that it may decrease the iteration time for the team as a whole.
The whole static / dynamic typing thing is its own flamewar waiting to happen, so I'm going to leave it at that.
I'd be surprised if a language with a Haskell-like syntax is verbose.
The verbosity most likely didn't come from the language itself, but from the proofs.
Once you've built the foundations, and proven a host of invariants about them, then you don't need to prove much more when you write the rest of the program. I bet Omega supports the very programming model you advocate: invulnerable foundations, and quickly written "rest of the program". If the code you saw was verbose, that's probably because it was foundation code. (After all, standard data structures are par of the foundations.)
To take a high-profile recent case: this would do nothing to prevent padding oracle attacks. Or future crypto attacks using techniques unknown to us now. Why? Because the encryption is working as it should. As advertised. As proven. Or imagine you used Rot13 for encryption.
Your DB could hold people's credit cards in clear-text; how will this language prevent that from happening?
Your website has no authorization tools, so you can access others' data by simply going to their URL; this is still a provably-correct logic structure.
And, more relevantly—how does the fact that a language can't fix those errors make preventing other errors a useless endeavor? It's true that there's no such thing as a programming language that can only write good/safe/acceptable programs, and a lot of people (myself included) who advertise programming languages as a solution to problems tend to overstate the relevance of type systems, correctness proofs, pure functions, &c, but that doesn't mean you can't eliminate a certain variety of error through good language design or by enforcing programmer rigor.
I wasn't intending to imply that, because language X does not solve likely-intractable problem Y, language X is worthless. Just that likely-intractable problem Y is likely intractable in language Z as well as X, as it's an inherent quality of the problem.
edit: I will however explicitly imply that more syntactically complicated languages are probably more likely to hide many kinds of logic errors. More brainpower spent decoding your code is more brainpower not spent analyzing your logic. Each to their own, clearly; I most definitely side with highly-readable code, and know several people who would likely feel right at home with Omega (e.g.: my brother is a math + philosophy double-major).
Studies like this tell me to never trust the opinion of a developer about programming languages and programming styles. In some cases not even my own. ;) Of course in this case we had not very experienced developers, but if we look at what expert developers often claim and how widely opinions differ I often have the impression that expert developers' fundamental opinions about programming languages aren't much better than that of a student.
"On average, subjective evaluation showed that students found transactions harder to use than coarse-grain locks, but slightly easier to use than fine-grained locks. Detailed examination of synchronization errors in the students’ code tells a rather different story. Overwhelmingly, the number and types of programming errors the students made was much lower for transactions than for locks. On a similar programming problem, over 70% of students made errors with fine-grained locking, while less than 10% made errors with transactions."
Transaction are felt as being of average difficulty, but they in fact spur far less errors. I bet we could find the same kind of bad judgement with "map" higher order functions vs "for" loops.
I don't think it is good argument against preventing known errors.
>Your DB could hold people's credit cards in clear-text; how will this language prevent that from happening?
You should specify that credit card information should be encrypted. For example, you define type "data CText value = ..." and two functions: "encrypt :: Key -> value -> CText value" and "decrypt :: Key -> CText value -> value". By requiring that certain table contains column of type "CText CreditCardInfo" you will be certain that you used "encrypt" and you won't mix your data with "CText Password".
Actually, TDD acronym can stand for Type Driven Design. And as you design your code around tests, you can design your code around types. The main difference is that logic errors will show up earlier and these typed invariants are proven, not tested.
So if you add another parameter to your cipertext data type, make it "CText algorithm value", change encrypt and decrypt to "encrypt :: Key algorithm -> value -> CText algorithm value" and "decrypt :: Key algorithm -> CText algorithm value -> value", you can require that that credit card info column should be "CText AES CreditCardInfo". You or your fellow programmer will be forced to provide that. And you won't succeed with ROT13 here.
No I'm not. When I say "no error", that include the specs. For instance, correctly following a specs when the green button set of the emergency shut down makes the interface too astonishing. That's a bug.
> Second, it's way more easy to take a bunch of common sense measures than to deal with this.
Of course. we never tried it seriously. What we didn't try yet is always more difficult. But if we do, it may very well become easier. I don't know.
Anyway, these weren't the point. My point was that the domains where we need bug-free code is broader than we might think at a first glance. Not being able to trust that the code you run is error-free has costs that could very well be more important than taking the time to prove the absence of errors.
LtU is just outright adorable sometimes.
- Sooner or later we'll go back to the moon.
- Sooner or later we'll understand how the brain works.
- Sooner or later the earth will crumble to dust.
...and so on.
But seriously, we've only been programming for 50 years now. There's still plenty of time for some revolutions and paradigm-shifting—just because the Mythical Man-Month has been heart-rendingly applicable for the last 50 years, doesn't mean that things can't change.
For example:
1. If everyone agrees to target some highish-level bytecode or another, every language will basically have access to every other language's libraries (let's hope it doesn't end up being the JVM, though things seem to be heading there.)
2. If we stick content hashes in function and class names, there will no longer be such a thing as API versioning conflicts, because you'll always know what you're calling—and you can just import random code from remote sites (i.e. invoking on a URL as an identifier = loading whatever bytecode is available at that URL), because you'll just hash it and guarantee that it matches its name before jumping to it.
3. If we can stop requiring that the source code we write be exactly the same source code the compiler parses, we can treat code files as a serialization format for an AST data structure (in XML or SEXPs if you want to keep the source-source human-readable), and work with it however we like in an IDE, even "rendering" it as one old-style-"language" or another.
And so on. These are problems that just need to overcome 20 or 30 years of inertia, and, ever-so-slowly, we're doing it.
Personally, I'm not a fan of runtimes. They don't give me the same warm, fuzzy feeling as compiling to native code and running directly on the OS.
What if the the OS's native code is bytecode? http://en.wikipedia.org/wiki/Singularity_(operating_system)
Re. 2: didn't we go through this when SOA and SOAP were all the best thing since sliced bread? The problem with APIs is not with versioning per se (if want to use URIs, just stick version number in the first position, webservices do that) - it's about what happens to dependencies. You have to call v5, you've got v1..v8 available, but another library you use talks to v3. Can you share objects? How is the v8-compatible state affected when v5 and v3 are doing the work? Which api is called when in your v5 area you call a method on a v3 object?
Re. 3: Yeah... I was considering tackling that for my degree at some point. The source file is just a placeholder that can contain some string generating new placeholders - why don't we simply start working on it that way?
Zope is an application server. In a given point in its history, Zope Corp, then Digital Creations, decided to "do it right" and fix each and every design wart from version 2 on version 3. The end result is that Zope 3 is more or less incompatible with Zope 2, specially with the kind of app we were developing with it in 2001 (IIRC).
A friend of mine joked Zope 3 should no longer be called "Zope", but, since "Z" is the last letter of the alphabet, the only reasonable choice would be "Yope" and that would suggest a step backwards instead of the jump forward it was.
With that in mind, I never built a product whose name started with Z.
There's a place for that, but the future of programming languages, in my mind, lies in changing the metaphor of the process from specification to experimentation. After all, the problem with the specification metaphor is figuring out what the specification actually _is_. To me, the best route to get there is experimentation.
Make programming more about experimentation and I think we'll get somewhere.
(I'm still going to read more about Omega. It looks interesting enough.)
I don't mean to keep throwing water on the fire but the research community already made trees that can't be unbalanced because they wouldn't typecheck, by encoding the depth of the tree into its type. Okasaki demonstrated the concept in Haskell, I believe. Getting it to work for RB-trees sounds new though.
From one of the authors of Epigram: http://e-pig.org
I heard they intend to include functionality of SHE into GHC.
It was Self with mathematical rigor and some MOP elements, IIRC.