Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

My first verified imperative program

markushimmel.de

Post reply on HN
Print view View original

101–105 of 105 posts

Re: My first verified imperative program

#101

Post by tsimionescu »

lmm wrote: post #94
tsimionescu wrote: post #86

Earlier quoted context omitted.

I believe you're misunderstanding the problem. The terminal doesn't "break" in the sense that it crashes or does something undefined for those cases. The terminal is doing something that is completely meaningful and well defined and probably has some realistic use cases, such as switching to a different character encoding. The only problem is that it's not what the user wanted to happen. For a simple example, if a fi…

> I believe you're misunderstanding the problem. The terminal doesn't "break" in the sense that it crashes or does something undefined for those cases. The terminal is doing something that is completely meaningful and well defined and probably has some realistic use cases, such as switching to a different character encoding. I'm aware of the details, but I think sometimes that knowledge leads people to miss the fores…

This is an entirely new claim - that the Terminal should try to understand what its input means. You can go ahead and try to implement this - I think you'll easily see that it's extremely hard to do so.

A terminal is basically a function foo(char_stream) = formatted_char_stream. It has no idea whatsoever what the input means, or what the output is supposed to mean. Your Ctrl-S example is completely in line with this: it's one control code that the Terminal chooses to display/interpet in a certain way (older terminals would just stop, newer terminals display some warning text and wait for user input). Recognizing that the start-red-output control sequence should not be interpreted as a control sequence if it's coming from the output of `ls` is a fundamentally different type of change.

Would it be nice to have a different concept, a CmdDisplayer that takes as input (commands, command text, control text) and outputs formatted text while understanding its input? Maybe. But it wouldn't be a terminal, and it would require a fundamental redesign of every single program that wants to meaningfully interact with it - especially all shells and any TUI program that might make the most use of such a tool.

Re: My first verified imperative program

#102

Post by lmm »

tsimionescu wrote: post #101
lmm wrote: post #94

Earlier quoted context omitted.

> I believe you're misunderstanding the problem. The terminal doesn't "break" in the sense that it crashes or does something undefined for those cases. The terminal is doing something that is completely meaningful and well defined and probably has some realistic use cases, such as switching to a different character encoding. I'm aware of the details, but I think sometimes that knowledge leads people to miss the fores…

This is an entirely new claim - that the Terminal should try to understand what its input means. You can go ahead and try to implement this - I think you'll easily see that it's extremely hard to do so. A terminal is basically a function foo(char_stream) = formatted_char_stream. It has no idea whatsoever what the input means, or what the output is supposed to mean. Your Ctrl-S example is completely in line with this:…

> This is an entirely new claim - that the Terminal should try to understand what its input means.

I don't see it as a different claim. My position is that the terminal should not move into a bad state for any valid input, and that a state that the user understands as being "broken" is probably a bad state. To my mind this should not require detailed understanding of what each program is doing, which I agree is difficult, but just some more basic things like making it clearer to the user why their terminal is in a funny state (and how to undo it), or perhaps ensuring that the terminal reverts to a good state whenever a program that had changed its state exits.

Re: My first verified imperative program

#103

Post by tsimionescu »

lmm wrote: post #102
tsimionescu wrote: post #101

Earlier quoted context omitted.

This is an entirely new claim - that the Terminal should try to understand what its input means. You can go ahead and try to implement this - I think you'll easily see that it's extremely hard to do so. A terminal is basically a function foo(char_stream) = formatted_char_stream. It has no idea whatsoever what the input means, or what the output is supposed to mean. Your Ctrl-S example is completely in line with this:…

> This is an entirely new claim - that the Terminal should try to understand what its input means. I don't see it as a different claim. My position is that the terminal should not move into a bad state for any valid input, and that a state that the user understands as being "broken" is probably a bad state. To my mind this should not require detailed understanding of what each program is doing, which I agree is diffi…

Having a way to return to the default would be nice, but it wouldn't fix the base problem that a program can't simply print a file name to stdout if it thinks stdout might be connected to a terminal. Even if the terminal didn't "break", it would still not display the file name in a useful way (e.g. a user couldn't copy paste it from there).

Re: My first verified imperative program

#104

Post by Joker_vD »

alternatex wrote: post #88
sureglymop wrote: post #64

Earlier quoted context omitted.

How so? If you specify the type int how would that save you from an overflow/underflow at runtime?

Not sure if types are supposed to protect against overflow/underflow, it's more in the arithmetic territory. Interesting idea though, I wonder if some programming language allows overflow/underflow checks directly in the types.

Yes, it's actually quite easy:

    +: (int, int) -> int    // or (int, bit) as the return type
    *: (int, int) -> int
etc. Those are the actual types of those arithmetic operations.

Re: My first verified imperative program

#105

Post by lmm »

tsimionescu wrote: post #103
lmm wrote: post #102

Earlier quoted context omitted.

> This is an entirely new claim - that the Terminal should try to understand what its input means. I don't see it as a different claim. My position is that the terminal should not move into a bad state for any valid input, and that a state that the user understands as being "broken" is probably a bad state. To my mind this should not require detailed understanding of what each program is doing, which I agree is diffi…

Having a way to return to the default would be nice, but it wouldn't fix the base problem that a program can't simply print a file name to stdout if it thinks stdout might be connected to a terminal. Even if the terminal didn't "break", it would still not display the file name in a useful way (e.g. a user couldn't copy paste it from there).

> it wouldn't fix the base problem that a program can't simply print a file name to stdout if it thinks stdout might be connected to a terminal. Even if the terminal didn't "break", it would still not display the file name in a useful way (e.g. a user couldn't copy paste it from there).

Well, I'm all for having something like a "raw copy" function in the terminal, but if a filename contains characters that can't reasonably be copy-pasted then there's not really anything that can be done about that (other than "don't give your files silly names"). I think having the terminal get into a bad state is a far worse problem; weird/corrupted filenames are something that happens and people generally figure out a way to deal with them.

Post reply on HN