Interestingly, that's exactly how I would describe reading Proust's Remembrance of Things Past. It's very hard to read at first, until you can get into the rhythm of the thing. For example, here's one sentence:
And so it was that, for a long time afterwards, when I lay awake at night and revived old memories of Combray, I saw no more of it than this sort of luminous panel, sharply defined against a vague and shadowy background, like the panels which the glow of a Bengal light or a searchlight beam will cut out and illuminate in a building the other parts of which remain plunged in darkness: broad enough at its base, the little parlour, the dining-room, the opening of the dark path from which M. Swann, the unwitting author of my sufferings, would emerge, the hall through which I would journey to the first step of that staircase, so painful to climb, which constituted, all by itself, the slender cone of this irregular pyramid and, at the summit, my bedroom, with the little passage through whose glazed door Mamma would enter; in a word, seen always at the same evening hour, isolated from all its possible surroundings, detached and solitary against the dark background, the bare minimum of scenery necessary (like the decor one sees prescribed on the title-page of an old play, for its performance in the provinces) to the drama of my undressing; as though all Combray had consisted of but two floors joined by a slender staircase, and as though there had been no time there but seven o'clock at night.
---
@pron: Most humans only reason very sloppily, if they reason at all. I don't see any good reason to cater to the lowest common denominator.
I didn't say anything about the lowest common denominator or sloppy thinking, but there is no evidence that suggests that the human mind works equally well with any arbitrary mathematical structure. A mathematical structure caters neither to the lowest common denominator nor to the most disciplined thinkers, but is, as far as we know, arbitrary with respect to human cognition. If it caters to anyone in particular, it is by chance.
My point is not that mathematical structure is bad -- far from it -- but there is no scientific basis to suggest a particular structure is particularly good. I read your comment as saying that a good mathematical structure implies a good mental structure, and I don't see what is the scientific justification for that claim.
Why would such a thing be necessary? Code isn't meant to be “perceived”, it's meant to be designed to meet a given specification.
As an extreme example, consider that life on earth displays all the desired qualities of programming -- abstraction, modularity and composition, maintainability, and it even supports complex ideas such as concurrency and meta-programming -- yet the language it is programmed in and evidently provides all these nice programming concepts looks nothing like ML. Why? Because it is optimized for a different kind of programmer. I think that if that programmer were forced to use ML, we wouldn't see any of those nice qualities or even a working system at all.
This means that programming qualities are not attributes of the language but of the interaction between language and programmer.
Not at all. A while back, I had a kidney problem that somehow managed to first manifest itself as incessant headaches. So much for modularity.
Modularity doesn't mean compartmentalization, or isolation, of failure, which is impossible in general (imagine a failure in the math module; checking that in other modules would be hard), although life achieves that relatively well, too. For example, a failure in a random number generation module will manifest itself in some strange ways in other parts of the system. In some ways, modularity and compartmentalization are sometimes at odds, with the latter requiring replicated functionality.
It's not impossible. There are two ways to do it:
(0) Static: Prevent the deployment of incorrectly constructed modules. Obviously impossible in an evolutionary setting (life).
(1) Dynamic: Require every module to check its own inputs, internal state and output. Admittedly, this is at odds with performance, which arguably matters most in a competitive setting (life).
In general, I wouldn't borrow inspiration from biology. Life forms are too busy trying to survive to bother being perfect. But programmers have a moral obligation to be Intelligent Designers.
As to the question of failure isolation, your solutions do not work in general. Proving that a component is correct is intractable for all computational models (even finite state machines) in general[1]. When it's done in practice, it is done at great effort, only on very small codebases, and even then at great cost both in effort and in design limitations. Checking the correctness of your input dynamically is also impossible in general because to know whether any arbitrary output of a black box is correct, the entire functionality of that black box must be replicated.
In practice, there are solutions of both kinds that are as effective as the effort required to produce them, which invariably means some compromise must be made.
[1]: See my post on computational complexity results of software verification: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
That's because, in general, any random system you can come up with is crap. Even if evolution was good enough for Nature, we need Intelligent Design. (Or maybe not for you. Maybe you're happy with crap programs that only “work” in a statistical sense. I'm not.)
> When it's done in practice, it is done at great effort, only on very small codebases, and even then at great cost both in effort and in design limitations.
Where you see a limitation, I see a source of relief from not having to explore a design space that mostly consists of crap I wouldn't want to use, let alone maintain.
Formal methods do work, and work very well, but not at all in the way people who have never used them on real-world systems think. Formal methods are on a spectrum of cost/benefit with an exponential curve of diminishing returns. For example, to go from, say, 98% confidence to 99.5% you need to expend about the same effort as going from 80% to 95%.
Forget arbitrary or "random" software. While there have been teams who have worked months or years on deductively proving some program correct, no team has ever been able to prove the correctness of even a mid-sized application. You can set your standards as high as you like, but we cannot at the moment figure out how to completely prove the correctness of real-world software of any significant size even in principle.
As for the kinds of formal methods that you use: Mechanical verification no longer convinces me. It turns out that I don't just want to know whether a program is correct. I also want to know why it is correct, which parts of the program are closely related to which parts of the specification, how easily the program can be modified to satisfy a slightly different specification, etc., and these questions aren't easily answered by mechanical verification tools. (“Tweak the system's definition, re-run the tool” is for obvious reasons not satisfactory.)
Considering that human understanding of the very systems we create should be the ultimate goal, I'd say that we shouldn't consider a system “proven correct” unless the proof can be communicated to a human. This means the proof itself should be short enough. If the proof requires running program to exhaustively verify a long list of cases (e.g., as done in the proof of the Four Color Theorem), at the very least the program itself should be short enough.
I used to think that 20 years ago when I was a young programmer. But then I've seen the requirements for an air-traffic control system. You cannot write one in fewer than a few MLOCs. Same goes for a modern operating system, or for an organizational software. It's always easy to say that about problem domains you're not familiar with. The world is very complicated and therefore so is software.
> I'd rather live in a world where every program in a high-level language is no longer than, say, 5KLOC, but those 5KLOC are perfectly well understood by their authors and anyone else interested.
Well, at the very least, that would be a world without computerized air-traffic control systems (I keep mentioning that example because that's something I worked on for some years). But the reality is that air-traffic control systems work, and thanks to them we can have many more airplanes in the air at any given time, and we very rarely get collisions.
Also, we don't know how to prove most real-world 5KLOC programs yet. The largest program ever completely verified was probably seL4, and that was about 10KLOC of C; hardly a high-level language by today's standard. But let's say it's comparable to a 5K program. Now, seL4 took about 20 man years to write by a team of expert academics. I know someone on that team and they're confident they can do that a lot faster now. He says he'd figure about 5 man years (optimistically). That's 1 man year for 1000 LOC, by an optimistic estimate. But that's not all. In order to keep the proof feasible, they couldn't just write any code they wanted, but were restricted to using only the simplest algorithms ("braindead simple" he called them).
> Considering that human understanding of the very systems we create should be the ultimate goal, I'd say that we shouldn't consider a system “proven correct” unless the proof can be communicated to a human.
I totally understand your wish that things were so, but there are results in computational complexity that mean this would be pretty much unattainable for most real software (even proofs of propositional calculus grow exponentially). I don't think you realize how small is the set of software that can be written in this way. But also, there's really no need. Why work so hard for simple software when we can get to similar failure levels as hardware with formal methods that are weaker than proof? Software doesn't live in a vacuum, and there's no point writing software for an airplane that's infinitely reliable if there's a real (albeit small) chance the wings might fall off.
Split it into several programs that can be verified independently.
> In order to keep the proof feasible, they couldn't just write any code they wanted, but were restricted to using only the simplest algorithms ("braindead simple" he called them).
Frankly, I can only see this as a good thing.
> but there are results in computational complexity that mean this would be pretty much unattainable for most real software (even proofs of propositional calculus grow exponentially).
This comes from the assumption that you first develop the system to be verified and only then verify it.
> I don't think you realize how small is the set of software that can be written in this way.
As if more software were automatically a good thing.
Doesn't help if the correctness of the whole program relies on an interaction of the component. See my blog post on the matter (the complexity of verifying a composition of k components is not only exponential in the number of components, but in the complexity of each; in other words, internal complexity cannot be hidden; this was proven in 2005 I think, by noting that the interaction of k finite-state-machines can simulate a nondeterministic Turing machine with a tape of size k).
> Frankly, I can only see this as a good thing.
Many of the algorithms that drive most progress in verification itself -- such as SAT solving and static analysis -- would themselves fall far short of this bar. Ironically, forgoing complex algorithms altogether would make verification even harder.
> This comes from the assumption that you first develop the system to be verified and only then verify it.
No, the two problems are of the same complexity. Developing a correct program can be no easier than verifying one. See my post.
> As if more software were automatically a good thing.
Well, that's a whole other discussion. In this one, I do not attempt to judge whether software is good or bad.
You're assuming that the components are allowed to interact with each other in arbitrarily complicated ways. IMO, if the complexity arises from the interaction between components, rather than staying confined within each individual component, you effectively still have one gigantic ball of mud.
> Many of the algorithms that drive most progress in verification itself -- such as SAT solving and static analysis -- would themselves fall far short of this bar.
Indeed. That's precisely why I'm not interested in mechanical verification anymore.
> Ironically, forgoing complex algorithms altogether would make verification even harder.
Perhaps. But it would also provide an incentive for exploring how much systems can be simplified. Maybe there are hard limits, but I don't think we're anywhere near reaching them.
> Developing a correct program can be no easier than verifying one.
The difficulty lies elsewhere: in the extremely low probability that an unverified program will be correct.
Look, you can talk about worst-case (i.e. general or arbitrary) and you can talk about best-case. If you read my blog post you'll see that real-world software has been found to hit worst-case verification complexity, but neither worst-case nor best-case is what we really want. We're interested in the common case, which requires years of empirical observation.
While it is certainly possible that we'll slowly be able to improve formal verification for the common case (as an industry user of formal methods, I certainly hope so and believe it will happen in a few decades), there is no current indication that this would ever be affordable. Currently, proof of correctness of anything larger than a few hundreds or a couple of thousands LOC is simply out of reach for the foreseeable future. So I'm not assuming anything, just stating the worst-case, and noting that there is no empirical indication that the common case is significantly better.
> That's precisely why I'm not interested in mechanical verification anymore.
Well, that's the only approach that has been shown to work in practice on real world software so far -- and they work very well (although, again, not quite in the way people who have not had experience with formal methods think). Deductive proofs (with Isabelle, PVS, Coq etc.) is used only to tie together results of automated methods, or fill in the holes where automated methods have failed. Doing it any other way is simply not economical. Even the most avid supporters of manual verification (who've actually tried it on nontrivial software) would agree. I don't think anyone believes that "ordinary" non-high-assurance real software (aside from certain very small core components) would be verified by deductive proof any time in the next few decades. The only people who believe otherwise are those who haven't actually tried formal methods on real-world software.
> The difficulty lies elsewhere: in the extremely low probability that an unverified program will be correct.
But software requirements aren't for 100% confidence in correctness, if only because you don't get anywhere near that with the hardware the software is running on. So the question is precisely how much more correct a software is with increasing verification effort. Like I said, there appears to be a pretty steep curve of diminishing returns. End-to-end verification is almost never affordable, but it is also almost never required.
What the formal methods community is really interested in these days is how to reduce the cost of verification required to achieve current (and near-future) correctness requirements.
You, perhaps. I'm interested in how much things can be simplified. It's a different kind of experiment: “If we prioritize simplicity and correctness, and say to hell with every other consideration, what kinds of programs can we write?”
> Deductive proofs (with Isabelle, PVS, Coq etc.) is used only to tie together results of automated methods, or fill in the holes where automated methods have failed.
I count fancy proof assistants among those technologies I don't want to have to trust anymore. When I read a proof script full of complicated tactics, my eyes glazeth over.
> I don't think anyone believes that "ordinary" non-high-assurance real software (aside from certain very small core components) would be verified by deductive proof any time in the next few decades.
If “real world software” presupposes this attitude of not wanting to do things the right way, I'm not terribly interested in it.
> But software requirements aren't for 100% confidence in correctness, if only because you don't get anywhere near that with the hardware the software is running on.
Hardware failure is Not My Problem (tm). I just want it not to be my fault when things go wrong.
> What the formal methods community is really interested in these days is how to reduce the cost of verification required to achieve current (and near-future) correctness requirements.
As I told other people, I'm not interested in “communities”.
I understand, but you must realize that we're not starting from scratch here, and we do know some things. The people who wrote, say, CompCert and seL4 did so with the exact same goals. It took them 20 man years for a small, pretty simple program, and they believe they can do it in 5.
> When I read a proof script full of complicated tactics, my eyes glazeth over.
Well, you should take a look at TLAPS[1], the TLA+ proof system. It's a structured, declarative proof language (Isabelle also has a declarative proof language called Isar), whose proofs look like those in the appendix of this paper[2], and are made to be readable to humans.
I should say that informal proofs of algorithms have not once and not twice been found (by automated tools like model checkers or by using structured proofs) to be wrong..
> If “real world software” presupposes this attitude of not wanting to do things the right way, I'm not terribly interested in it.
The "right way" isn't a decree from God. What's right for real-world software is dictated by its requirements, which include functional requirements, performance requirements, maintenance requirements, security requirements etc.. A software that's build the "right way" is one that meets its requirements while spending as little as possible to do so. A recpie app that has zero bugs of any kind and takes 7 years to build is not built the "right way", just as one-use plastic cups built with carbon fibers and costing $10 a piece is not built the right way. A recipe app shouldn't lose your recipes, but other than that, wanting to ensure no GUI bugs of any kind shouldn't drive up its cost much.
> I just want it not to be my fault when things go wrong.
Yes, but your customers wouldn't want to pay you 10x or 50x as other developers just to make sure your software doesn't have bugs of the type they don't really care about, nor do they want or need 0 chance of critical failure from your software. You can make make the chance of a critical problem being your fault extremely low without waterproof end-to-end verification. How much more will you be willing to invest to drive those chances from 10^-7 to 10^-8?
> As I told other people, I'm not interested in “communities”.
Well, you can be interested in building a spaceship that can go faster than light by warping space and not be willing to compromise on anything less, but if there's no one in the research community but you working on that problem, your chances of actually flying in such a spaceship are slim. I think that at the very least you should want to know about past and current research and its findings, if only to save you a lot of repeated work.
What's the structure of the hopelessness and anguish expressed in Moby Dick? What can you look at that would be a reasonable expression of the twists and turns of Dune?
Paintings can express abstract concepts as well, but I think they're hard pressed to express multiple convoluted ones with cause-effect mechanics succinctly.
They may be ineffable to computers (at this time), but they are not ineffable to us. We can ascribe meaning to these words, and programming languages do the same thing. They provide a language with common meanings that both a compiler and humans can understand.
btw, Qualia is a meaningless concept to me, not ineffable; concepts definitely are. On the other hand, some philosophical ideas might just be plain wrong and thus not possibly translate to code that had to be logical (unambiguously). Why wouldn't there be logic behind?
> Quale: A property considered separately from a thing having that property
I just don't like the word. Why not call it property?
> qualophile: A cognitive scientist who endorses qualia as being unmeasurable by heterophenomenology.
That's new to me, but yeah, when I hear the term it is used to describe properties that are not discretely measurable and to me those might as well just not exist, or wrong as far as that relates to the grand parent post.
There's a bunch of 'block based' programming languages that some educators are using to teach programming. Searching for 'Blockly' turned up https://developers.google.com/blockly/, but they're definitely not the only game in town.
Way back when Charles Simonyi created this thing he called "Intentional Programming" (https://en.wikipedia.org/wiki/Intentional_programming). As near as I can tell the big idea is that instead of encoding the program in textual source code you'd instead store the program in a parse tree/etc (I'm not super-familiar with compiler details - it's some sort of tree that represents the program, semantically). Your IDE would then enable you to interact with it however you wanted (as text, as blocks, etc, etc).
So yeah - text is king, but there's a lot of other really interesting options out there, too
If I have a bunch of libraries that more or less do what I want and all my program has to do is glue them together (this is common in scripting scenarios), then I could just draw it up in a GUI like Gephi and cross-compile it to a script, instead of writing the script by hand. Complete separation of data flow from the implementation of that flow.
I imagine you could do this pretty easily in a language like Haskell (since everything is a function call) or Lisp (where everything is "data") so you don't have to implement special logic to figure out how particular nodes should behave. You could also do this for "explicit" DAG engines like Make, Airflow, and Luigi.
[0]: http://www.graphviz.org/content/dot-language [1]: https://knsv.github.io/mermaid/
EDIT: this ([2]) turned up in my Googling. I suppose there's a good reason nobody uses it?
If you are interested in this you should check out a company called Mendix, which is building a SaaS platform for building applications using graphical tools, and the Eclipse Modelling Framework, which is a huge project aiming to add modelling and code generation capabilities to Eclipse (in my experience it is slightly academic, in the sense that you often encounter bugs or cryptic errors in practical use).
There are upsides an downsides to this paradigm of course; one downside is that it's not obvious how to read control flows at first. On the upside, having all your functions available in modular form makes if far easier to explore and program using high-level concepts. What I hate about conventional programming is all the typing and having to remember all the function parameters, calling conventions etc., I want the computer to do that for me. Writing code in an IDE is about as enticing as making my own Lego bricks from scratch.
Unfortunately they're still constrained by the language itself being designed around text. A lot more could be done with a language+IDE developed in tandem, with the IDE's needs always taking precedence in decisions.
I would agree that diagrammatic programming is a process that inherently seems like it would solve the opaqueness of programming.
But I'd say this paradigm is just as much inherently limited and not useful for "serious" work. This is because the multitude of "parts" that a computer program has exist in too large a space to be visually represented and because the details don't really follow our intuits for two or three dimensional objects.