 |
|
|
|
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Darren New <dne### [at] san rrcom> wrote:
> But honestly, I've never seen code where which element gets accessed
> next is obvious to a programmer but not to the compiler. I've never seen
> code where you could prove to a person's satisfaction that it was
> correctly accessing the array but couldn't prove it in a formal way
> given what's in the code itself, assuming you have all the code in front
> of you, of course.
Of course everything can be proven formally. The problem is how hard it
is to prove it. If you need to be a mathematician to formally prove that
certain values always keep within certain boundaries, that can be pretty
demanding for a programmer.
One practical situation where it may be hard to prove you never access
out of boundaries is when you have a dynamic hash table, where the elements
at a certain position form a linked list, but all the elements are still
stored in the same dynamic array. Each element is a pair: The data, and an
index to the next element in the linked list. When you search for a value,
you calculate the hash index (which can already be hard to prove to be
inside the dynamically-sized has table), and check if the value is at that
position. If it isn't, you take from that position the index to the next
position and check that, etc.
Assume that elements can be removed from the hash table, and that the
hash table array size can be reduced if enough elements are freed
appropriately. Naturally you would now have to prove that all the indices
left in the hash table point to valid indices in the now-smaller hash
table. In other words, it's not enough to prove that indices are valid
when you insert a new element in the hash table, you also have to prove
that the existing indices keep valid when the size of the hash table is
reduced.
I would be pretty impressed by the programming language where you are
even able to express that.
Intuitively proving this to a human could be much easier (although
it would probably not be a formal proof).
--
- Warp
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Orchid XP v8 <voi### [at] devnull> wrote:
> Not so many years ago, software that wasn't 100% crash-free was
> unacceptable. Today this is considered "normal". And it's all due to M$.
OTOH, 20 years ago most serious operating systems (and consequently other
software) were running huge servers with hundreds, if not thousands of
users.
This was rather common especially at universities and other similar
academies: You were lucky if you had access to an actual desktop computer.
Usually all you got was a dumb terminal connected to the main server,
which was used by hundreds of others at the same time.
Back then it was completely unthinkable that the server would crash
randomly. It was more or less an assumption that the server could handle
without problems hundreds of simultaneous users logged in, all of them
running a half dozen of programs, and most of them using the internet
(or other network).
Today the situation is more or less reversed at those same places:
You are lucky if you get to log in into a big server. Instead, you are
usually stuck with a crappy desktop computer (usually running Windows,
but if you are really lucky, Linux).
AFAIK, in many of those places they run weekly - if not even nightly -
restores to all the desktop computers automatically (ie. wipe the system
clean and put a fresh copy of the system from a network disk, or whatever),
rather than to wait for them to rot. (Usually student files are stored in
a network disk rather than the computer itself.)
--
- Warp
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Warp wrote:
> Of course everything can be proven formally. The problem is how hard it
> is to prove it. If you need to be a mathematician to formally prove that
> certain values always keep within certain boundaries, that can be pretty
> demanding for a programmer.
Fair enough. I guess the research is in making it easier to prove.
Apparently the stuff for proving Ada (or rather the subset called
"Spark") is valid lets you do proofs by induction and by contradiction,
which seems pretty ... intense.
> One practical situation where it may be hard to prove you never access
An excellent example. Thanks.
I'm wondering if it's really as hard as it sounds, *given the code*.
Obviously the hash is going to have to be taken modulo the table size,
for example, and storing the link into the hash table is going to have
to calculate the link somehow. I think by leaving out the details, it
might look harder to prove than it is. Given the code for calculating
what the next link would be, and where to store it into the table, it
might be pretty obvious you can't run off the end.
Of course, shrinking the table might also be either really hard, or less
hard, to prove, depending on the actual code that decides when to shrink
the table. How does the code know it's time to shrink the table? The
same code that checks there aren't pointers off the end of the table
would be able to prove that it's safe to shrink the table.
If you actually have such code you could show, that would be cool.
Otherwise, yah, it's probably a good example. Something like B-tree
maintenance could be interesting to look at.
> I would be pretty impressed by the programming language where you are
> even able to express that.
Here's an example out of the Spec# document, for inserting into a
variable-length array:
one can specify the postconditions of Insert as follows:
void Insert(int index , object value)
ensures Count == old(Count) + 1;
ensures value == this[index ];
ensures Forall{int i in 0 : index ; old(this[i]) == this[i]};
ensures Forall{int i in index : old(Count);
old(this[i]) == this[i + 1]};
{ ... }
(Which basically says the array is one larger, the element you passed in
shows up where you said, the ones before didn't change, and the ones
after moved up one.)
So indicating that all the second elements of the entries in the hash
are less than the size of the hash is just a Forall expression there.
Forall(int i in 0 : hasharray.size; hasharray[i].next < hasharray.size);
Now, of course, proving that without a runtime check is the hard part.
> Intuitively proving this to a human could be much easier (although
> it would probably not be a formal proof).
Hmmmm... Hard to say, really. Certainly it would be easier to be less
precise, but I'm not sure it would be easy to *prove* it to a human than
it would be to prove it to a machine. For example, it's pretty easy for
a compiler to prove a binary search is safe and to remove the runtime
checks from that.
Correctness, yes. But safety? I'm still unconvinced.
As in, it could be much easier to prove for a text editor you'll never
overflow the screen buffer than it is to prove that the sequence of
operations you do to insert a line of text on the screen actually leaves
the screen looking how you'd expect it to. The types of things you want
to prove for a safe language are actually rather constrained compared to
"proving this program matches the specs."
Personally, my take is that if you can't formally prove your code
doesn't have holes in it, the run-time check is probably worthwhile at
that point, if you're actually interested in the robustness of your
code. If performance is a problem, put in enough asserts that the
runtime checks happen outside the hot spots instead of inside the hot
spots.
--
Darren New / San Diego, CA, USA (PST)
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Warp wrote:
> OTOH, 20 years ago most serious operating systems (and consequently other
> software) were running huge servers with hundreds, if not thousands of
> users.
... but still running a fairly small collection of software compared to
what tends to run on machines today. The Linux boot partition today is
multiple times the size of the biggest hard drives you could put on
"desktop" computers 20 years ago, and orders of magnitude bigger than
the disk space available on a mainframe 40 years ago. 10 years ago I
was impressed when the boss brought in a Windows machine with 128Meg in
it. Nowadays you can't even boot Windows in that, let alone do something
useful.
And of course, the hardware is flakier too. That's why NASA puts
20-year-old technology into satellites and space ships. You read the
google papers, and you see they run some job and it takes on the average
1000 machines, 7 minutes, and during that time on average two machines
will have some sort of hardware failure. Your software can seem really
flakey when your swap space has an unreliable sector in it - btdt.
Plus, software changes much faster today. People in a university aren't
going to use a compiler last updated (except for bug fixes) 10 years
ago. Nobody these days uses a C++ compiler last updated before the STL
was created. Nobody uses a database engine that has been stable for 10
years, or even an OS that has been stable for 10 years.
It's easy to make a system that doesn't crash. Get it working, then stop
dicking around with it. Windows servers are quite reliable, for example,
because people don't install new stuff and then take it off, plug in
random USB devices, try out new screen savers, etc. They're very careful
with their upgrades, just like they are for Linux.
> This was rather common especially at universities and other similar
> academies: You were lucky if you had access to an actual desktop computer.
Given the power of desktop computers 20 years ago, I'd disagree with the
"lucky" part of that. ;-) The stupidest thing the CIS department did at
my undergrad school was to start teaching assembler on Commodore PETs
instead of on the mainframe.
--
Darren New / San Diego, CA, USA (PST)
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Darren New <dne### [at] sanrrcom> wrote:
> The Linux boot partition today is
> multiple times the size of the biggest hard drives you could put on
> "desktop" computers 20 years ago, and orders of magnitude bigger than
> the disk space available on a mainframe 40 years ago.
There's no such a thing as "*the* linux boot partition" with regard to
size. You can create a bootable linux partition (with the latest kernel
and many utility programs) which fits on a floppy disk, so that you can
boot with it.
> > This was rather common especially at universities and other similar
> > academies: You were lucky if you had access to an actual desktop computer.
> Given the power of desktop computers 20 years ago, I'd disagree with the
> "lucky" part of that. ;-)
I believe you are old and academic enough to have used VT terminals.
I'm not sure which one I would prefer, an old desktop computer or a
dumb VT terminal... :P
(Yes, I am old enough that I got to the University here early enough
that VT-220 terminals were still in common use. I read my email, the news,
made programming assignments and even played batmud with those terminals.
The Internet was still a new thing that practically nobody had. Ah, the
memories.)
--
- Warp
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Warp wrote:
> There's no such a thing as "*the* linux boot partition" with regard to
> size. You can create a bootable linux partition (with the latest kernel
> and many utility programs) which fits on a floppy disk, so that you can
> boot with it.
Whatever. Fine. "*My* Linux boot partition." Happy? Sheesh.
A *floppy* is still more space than most mainframes had available in RAM
30 years ago.
> I believe you are old and academic enough to have used VT terminals.
> I'm not sure which one I would prefer, an old desktop computer or a
> dumb VT terminal... :P
Well, there is that. :-) Of course, the hard-copy terminals were handy,
given we were using a mainframe with a file system sophisticated enough
you could edit a file you'd printed out and still be able to edit it
again later without a lot of hassle. (E.g., you didn't get whole new
line numbers in your compiler errors because you added a bit of code
near the top.)
I do remember appreciating that the only way to edit on the glass ttys
was to use the 1200 baud connection in the sys admin's office.
> The Internet was still a new thing that practically nobody had. Ah, the
> memories.)
I don't think there was even internet access around until after I
graduated. It certainly wasn't cheap enough that a school as small as
mine was going to pay for it. Wasn't until grad school I got that. Altho
I did hang out on compuserve for a bit.
--
Darren New / San Diego, CA, USA (PST)
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Invisible wrote:
> Well, currently a program's arguments are just a giant blob of text. The
> OS does nothing more than hand it over to the program, which may then
> interpret them in any way it pleases. This is LCD; it works for
> everything, but it's not terribly sophisticated.
>
> How about if, say, the program could somehow "tell" the OS what
> arguments it actually accepts? (In the same way a program file usually
> contains metadata to "tell" the OS all kinds of other stuff about it,
> such as linking information.) Then the OS could report invalid argument
> names without even needing to bother actually starting the program
> itself. And just think of the auto-complete possibilities.
>
> Hey, let's go one better. The majority of CLI arguments are either
> on/off switches or filenames, right? Well what if we *tell* the OS what
> things are on/off switches, and that their default state should be? What
> if we *tell* it which things are supposed to be filenames? (And whether
> the name in question *should* or *should not* exist when the program is
> run? Or whether it should be a *file* or a *directory*? Or maybe even
> the name of another program?)
You don't need a whole new OS for that.
Recent versions of bash come preconfigured for smart autocomplete. Random
example:
apt-get remove <tab> completes package names you already have installed.
Or look at fish (my current shell). It colors the stuff you type in real
time. Type ls --srot and it will show red, so you know you
mispelled --sort.
http://www.fishshell.org/screenshots.html
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Nicolas Alvarez <nic### [at] gmailcom> wrote:
> Recent versions of bash come preconfigured for smart autocomplete. Random
> example:
> apt-get remove <tab> completes package names you already have installed.
I like the smart autocomplete in zsh. For example, if I write this in zsh:
mplayer -su<tab>
it will autocomplete it to "mplayer -sub", but since that's not the only
possible valid completion, if I press tab again, it will list all the
possibities:
mplayer -sub<tab>
-sub -- use specified subtitle file
-sub-bg-alpha -subcp -subfont-osd-scale
-sub-bg-color -subdelay -subfont-outline
-sub-no-text-pp -subfont-autoscale -subfont-text-scale
-subalign -subfont-blur -subfps
-subcc -subfont-encoding -subpos
The autocompletion of file names is also application-dependent. For
example, if I have three files in the current directory, let's say
test.txt, test.cc and test.pdf, if I write this:
acroread t<tab>
it will directly autocomplate to "test.pdf" because that's the only one
of those files which is valid for acroread.
Also if I have a bunch of files whose names start with a 't', and all
of them have the access rights "-rw-r--r--" except one, which has the
rights "-rw-------", and then I write this:
chmod og+r t<tab>
it will directly autocomplete to the only file for which that command
makes sense (ie. the file which didn't have the +r rights already).
--
- Warp
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Warp wrote:
> The autocompletion of file names is also application-dependent.
FWIW, bash does this too. I suspect perhaps the zsh configuration files
are more complete, but I've been annoyed by trying to autocomplete the
destination directory of a "mv" command that wasn't writable and getting
ticked that the autocomplete just stopped working. :-)
--
Darren New / San Diego, CA, USA (PST)
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Warp wrote:
> Nicolas Alvarez <nic### [at] gmailcom> wrote:
>> Recent versions of bash come preconfigured for smart autocomplete. Random
>> example:
>> apt-get remove <tab> completes package names you already have installed.
>
> I like the smart autocomplete in zsh.
Bash can do that too. It's just stupidly disabled by default.
From fish design document:
"A special note on the evils of configurability is the long list of very
useful features found in some shells, that are not turned on by default.
Both zsh and bash support command specific completions, but no such
completions are shipped with bash by default, and they are turned off by
default in zsh. Other features that zsh support that are disabled by
default include tab-completion of strings containing wildcards, a sane
completion pager and a history file."
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
|
|
