"When mathematics made its way to software the notion of rigor hardened to a sort of math envy. Endless man-years have been spent trying to "prove programs correct" rather than to do computer-aided proofs as a human activity. But the best practitioners have always known that you can't take the human out of the proof life-cycle."
Reflexively, I don't like drawing a distinction between human activity and mathematics. What else in the universe does mathematics except humans?
Any field is going to keep humans in the loop or else it won't be useful to humans. Any field is going to strive to minimize humans' responsibilities in the loop or else it won't be useful to humans.
Right now I'm in the mood to drill down on "field" and "useful." A "field" implies there's some kind of shared research going on, and "useful" implies that it comes in handy for people's naive needs. (Who knows if something that's useful is really beneficial?)
Shared research, in itself, crucially involves summaries and citations to cash in on prior work. But when we snapshot these summaries and citations (e.g. writing them on paper), the discreteness of our snapshots permeates into discreteness of the citation expressions, which then permeates into discrete methods for locally assessing the value of the research, which then permeates into discrete valuations of the research. So I suspect this one useful application domain -- that is, the meta-theory of snapshotted shared research -- is sufficient to give a strong identity to the field of logic[1], regardless of what culture currently surrounds it and what other application domains intersect with it.
[1] I thought I was going to say "mathematics," but "logic" is a culturally closer term for what I described. The impression I've gotten is like this: Logic gives you a canvas for reasoning. Mathematics equips that canvas with intermediate scaffolding for the subjects you care about. It's paint by number! :-p
---
"Just look at ACL2."
Er, what about ACL2?
---
"The most harmful result of this slippery slope has been to enshrine and ossify notation as something most programmers are to be prevented from changing."
For at least this reply, I'd like to break down "harmful" into "less useful" and "less beneficial."
A programmer will find it more useful to be able to use the notation of their choice, especially notation of their own design. However, if many programmers each willingly stray from standard notations, they make the world of program code less useful in at least one way, to at least one audience: Newcomers face a steep learning curve, encountering different notations everywhere they look.
As for whether this is "beneficial" one way or the other, I don't know. I just wanted to cast doubt on the moral connotations of "useful" again.
---
"We don't pay nearly enough attention to the fact that large programs can't be taken in at a glance, and so at large scales the visual effects of notation must be subordinated to a tactile feedback-based environment."
I don't know if they can be completely "taken in," but making them interactive is great. Logic (in the sense I described above) is already essentially interactive because of the process of tracking down citations to convince oneself of any pieces that are hard to believe. It would be pretty useful to be able to navigate a program to see various views that are bite-size enough to take in.
Ooh, as an extrapolation of your unit-test-based ideas, it would be especially nifty to view a codebase as a fractal pattern where every possible run-time state corresponds to one location in the fractal. XD Do just enough fuzzing to draw a good density of pixels for the overall program fractal, render the errors in red, and then do more localized fuzzing when the user zooms in. Some design flaws and corner cases may be visually apparent without even being proper errors!
If you're starting with a conventional assembly language, you can probably display each subroutine call as a pyramid of the calls that happen inside, with each level being some fraction as tall as the previous one. Conditionals would be treated similarly to calls, except that they don't always happen, so sometimes they can be omitted from the inner levels of a pyramid. Non-call, non-conditional statements would be omitted from the fractal altogether to save room.
Sorry, I guess I got carried away on a specific idea. XD Your ideas are already pretty nice too.
I've been confirming my biases :) along similar lines this year, and ended up with some surprising conclusions.
It's easy to forget, surrounded as we are with computers, that mathematical proofs were not intended to be "rigid" the way programmers understand the term. Proofs were intended to persuade other mathematicians. Standards of rigor varied depending on who the audience was.
When mathematics made its way to software the notion of rigor hardened to a sort of math envy. Endless man-years have been spent trying to "prove programs correct" rather than to do computer-aided proofs as a human activity. But the best practitioners have always known that you can't take the human out of the proof life-cycle. Just look at ACL2.
The most harmful result of this slippery slope has been to enshrine and ossify notation as something most programmers are to be prevented from changing. A particularly startling experience was to reread Ken Iverson's great Turing Award lecture, "Notation as a tool for thought" (http://www.eecg.toronto.edu/~jzhu/csc326/readings/iverson.pd...) keeping in mind what I wrote earlier. Before programming existed, if a mathematician wanted to change his notation, he did so with the stroke of a pen and without a second thought. Now here's a great programmer, at the very outset, simultaneously holding math up as the gold standard for notation and claiming the flexibility of its notation to be self-evidently deficient.
I'm mostly preaching to the choir about syntax enhancement, given this is a lisp forum. But I'd argue that even lisp doesn't go far enough. We're still obsessed with finding the ideal visual notation to let a program be taken in at a glance. We don't pay nearly enough attention to the fact that large programs can't be taken in at a glance, and so at large scales the visual effects of notation must be subordinated to a tactile feedback-based environment.
Lately I've been building such an environment from scratch. It'll support programming in a sort of assembly language, not just to ease my implementation burden but also to explore if a good environment might reduce the need for a high-level declarative language. Concretely, the environment will log scenarios tried out during development, recording inputs and outputs for all function calls. The binary log will augment the version control history of a project, so that you can clone a repo, download its log and then start seeing warnings anytime you make a change, something like "hey, somebody tried this function with these inputs last week, but got a different output. Would you like to a) override that output, b) pin it as a unit test that must always pass, or c) tag this function as stateful so you don't see these warnings again?"
Beyond that initial use case, I want to make it easy to do things like:
a) Create a test with a single keystroke or gesture,
b) Visualize the space of input for a function as examples organized by different code paths taken,
c) Explore how the set of inputs tried has grown over the version history of a function,
..and so on.
I'm very surprised with this goal; nobody started out more notation-obsessed than myself.
The use of mathematical formalism is a practice that has a certain cultural context, and that context is often unfair. Furthermore, formalized ideas are as rigid and neutral as they can possibly be, so it's highly questionable to say people "should" express ideas this way, as though being rigid and neutral is morally right. There's no easy answer, because the cultural process of deciding what's fair or moral can also have effects that are unfair and immoral. For these reasons, it's quite understandable to pursue alternatives to mathematics, and this year I've been particularly interested in how those alternatives might work and succeed. This might explain the shift you're seeing.
Personally, I was very literal-minded as a kid. If someone couldn't tell me exactly what they wanted from me, right down to a fully executable program, I assumed they were either being maliciously equivocal or that someday they'd make a serious error: Genies, robots, aliens, and cartoon tricksters don't allow much tolerance for vagueness, so what cushy precedent would it set if I allowed vagueness to go unchecked?
So I may at some points build up to or rationalize vagueness in terms of precise reasoning, but I don't mean that as an endorsement of precise reasoning. It's a quirk of where I'm coming from.
I have been embracing less precise ways of thinking this year, but I've been using logic as a stepping stone toward vagueness for a long time.
If an abstraction leaks, for instance by allowing reverse engineering, we can usually fix this without any code changes: Just change the language docs to say that abstractions like this one are explicitly noncommittal about whether people can reverse-engineer them. If we don't like the abstraction once its idiosyncrasies are out in the open like that, we can develop an abstraction we do like and use that instead.
I don't think I ever liked these leaks, but elegance and convenience has kept me away from exploring alternative abstractions myself.
I had more to say on this all along, but I didn't have the time to write it out.
---
Performance-wise, it's interesting to keep CSS's abstractive power relatively simple, because (naively[1]) the relationship between N CSS rules and M DOM nodes has an overall complexity on the order of (N * M). Since it's pretty easy to understand the optimization of minimizing file sizes, programmers will just so happen to optimize this N factor without thinking about it. But if CSS had abstractions, the file size wouldn't correlate with N anymore.
Programming-in-the-small-wise, CSS properties are designed in a natural-language like way. What I mean is, there are lots of defaults, and there's often more than one way to specify the same formal behavior, so it's relatively easy to get something to work by taking small steps and guessing. Visual feedback further supports this style of trial-and-error programming.
Programming-in-the-large-wise, CSS is already full of ad hoc special-case interactions between properties to support the defaulting behavior I just described. This means it would be easy to make leaky abstractions. Even the meaning of "90%" depends on what property it appears in, so number-valued variables would likely have a few gotchas all on their own. If abstractions are leaky in practice, their programmer-given names will often be deceptive about their actual functionality, making large programs even harder to comprehend.
So adding abstractions to CSS would tempt people into an in-the-large programming style that not only fails to solve in-the-large maintenance problems, but also complicates performance and puts pressure against having a smooth CSS learning curve.
[1] I expect it's much more expensive than that due to text flowing, but also somewhat time-cheaper (albeit more space-expensive) if indexes or memoization are used.
---
For language design in general, recently I'm interested in finding ways to program without discrete abstraction boundaries or steep learning curves. I've often found CSS inspiring as an example of a language that invasively fills in details of another structured program (in this case a DOM), not to mention that it's an example of a continuous reactive language.
On the other hand, I'm interested in Turing-complete programming, I'm interested in programs that combine the efforts of independent library developers, and I'm interested in network services that have synergy despite having independent maintainers. Some kind of abstraction seems necessary for those things, but I'd rather find abstractions that leak in the right ways to correspond to the abstraction leaks in reality.
For instance, independent library developers or service maintainers aren't strictly independent as long as any user cares about both of them at once. It's often feasible for the user to prod the two projects to work together, or for the user to create or promote another project that makes that interaction irrelevant. Open source ideology and reverse engineering play into this, making it easier for users to manage these collisions. Abstractions, on the other hand, typically work against it. If an abstraction can be leaky in just the right way to be easy to reverse-engineer, that would be an interesting option here.
I'm submitting this because I found the first half of it to be a pretty interesting point of view. The latter half isn't bad, but it retreads a lot of the same ground.
Since Arc compiles each Arc expression to MzScheme before executing it, and since MzScheme compiles each of those expressions, Arc inherits this on-demand compilation behavior.
Well, since you ask. :-) And since the judging is all done, I might as well update it. So. Currently things are broken up into "dyn-cont", which has the Arc interpreter, "arc-boot", which is the code the interpreter will run on startup, and "memory-system", which is where I'm prototyping the stuff the next version of "dyn-cont" will run on: fake assembly code, which is a preparation for writing real assembly code.
1. Arc generates html and css from code. Search for "defop news.css" in news.arc and you'll see it.
2 and 3 are more complex and will require custom code. http://hubski.com has both but they've been added over several years as the creator got more fluent with arc. You can ask them what they did.
The GCC only supports a handful of Algol-family languages, and not a single Lisp. Arc is currently an interpreted language running on top of MzScheme. It's two different realms entirely.
Waterhouse wrote an Arc interpreter on top of Arc with continuations, and first-class macros and first-class special forms. Scanning over his submission form (http://lispinsummerprojects.org/static/summer/250119.pdf), it also interestingly lets quasiquote be defined as a macro.
To explain further: I ask if you're specifically looking for a compiler because some people think that the only way to run any code is with a compiler, or that specific languages require one. Absent a specific thing in a spec ("an implementation of AwesomeLanguage requires compilation or it can't be called AwesomeLanguage"), languages can be interpreted or compiled.
So if you're interested in compilers, and want to see one for Arc, that's fine. But the default way of running Arc is not with a compiler. If you just want to run Arc, follow the instructions above.
Thanks for reporting this! I bet this happened because of the HN redesign. There was some other stuff that broke on the site when that happened: http://arclanguage.org/item?id=18744 . I'll email the people at YC that can fix it.
Until they get it fixed, you can try Anarki instead. Anarki is a fork of Arc that's been changed somewhat, both to fix bugs and to add features. https://github.com/arclanguage/anarki .
