Hacker News new | past | comments | ask | show | jobs | submit | dmd's comments login

For people who enjoy this sort of thing, vaguely related is this puzzle: https://dmd.3e.org/a-shell-puzzle/

Oh, you're the author! I didn't notice and sent you an email, but will repost here:

    $ for i in 3 4 5; do f=puzzle.$i; echo $f: $(head -1 $f | wc -c); tail -$((i-1)) $f; ./$f; done
    puzzle.3: 1
    futz
    futz
    ./puzzle.3: line 3: futz: command not found
    puzzle.4: 1
    futz
    futz
    futz
    ./puzzle.4: line 4: futz: command not found
    puzzle.5: 1
    futz
    futz
    futz
    futz
    ./puzzle.5: line 5: futz: command not found
Does this count?

The entire point of using formal methods is that testing will never, ever catch everything.

Whereas, formal verification only catches what properties one correctly specifies in what portions of the program one correctly specifies. In many, there's a gap between these and correctness of the real-world code. Some projects closed that gap but most won't.

Can't you use the formal model to write/generate a lot of unit tests to verify the actual code behaves like the model does?

In most domains you're always going to have the possibility of a gap.

The real thing though, is that if you have a verified formal model and a buggy implementation, then _you know_ your problem is at that model <-> implementation level.

Could be the implementation is wrong. Could be that the "bug" is in fact not a bug according to your model. But your model isn't "wrong". If your model says that A happens in condition B, then that is what should happen!

You can avoid second guessing a lot of design patterns with models, and focus on this transitional layer.

If someone came up to you and said "I built a calculator and with this calculator 1/0 becomes 0" you don't say "oh... maybe my model of division is wrong". You think the calculator is wrong in one way or another.

Maybe the calculator's universe is consistent in some way but in that case its model is likely not the same model of division you're thinking of. This eliminates entire classes of doubt.


We should have formal verification of the formal verification specification. Standing on a turtle.

I've heard that called "validation". In other words, you verify that your solution meets the problem specification, but you validate that your specification is actually what you need.

You're looking for foundational, proof-carrying code with verified logins. I can't find the verified logic right now, though. Examples:

https://www.cs.princeton.edu/~appel/papers/fpcc.pdf

https://hol-light.github.io/

I'll also add that mutation testing has found specification errors, too.

https://github.com/EngineeringSoftware/mcoq


No matter how many times I do number 20, I end up with 615. Am I wrong, or is the solution sheet wrong?

I think you're right and the given answer of 596 is wrong. It's 380 m-w, 190 m-m, 45 w-w handshakes, so 615 in total.

Yeah. It's not even the only wrong answer on the page, which is troubling.

And as a dessert topping!

No, It's a FLOOR WAX!

Oh wow I (American) didn't even remember until seeing this thread that loo meant that.

I hope anyone who uses something like this has the grace to fall back to https://linux.die.net/man/1/dialog for non-GUI users. Or https://github.com/Textualize/textual if they want to be faaaaancy.

Well, after a bit of fiddling, Textual also worked on my Android running Termux.

Spiffy!

I like this one a bit less than I do the all text mode, though I will have to go through a bunch of widgets to see if that remains true.

Requiring Python seems a bit excessive, compared to the other one with works more lime the author intended, I believe.

Thanks for these. Interesting to look at.


Textual is new and fancy. Dialog has been on pretty much every linux system for a quarter century.

Yes. It shows. I like that quarter century stuff.

On my Note phone, I just tried dialog. Spiffy!

I used Termux, and did this for a hello world:

     pkg install dialog
     dialog "hello there" 20 3
And BAM! There it is rendered in text, easy peasy.

Thanks for the reference. I agree with you.


Or for those won't don't want to install dialog, just do your ui forms directly from the shell: https://github.com/polijan/sourcedialog

man that's an ugly man page. The FreeBSD one is a lot easier to read.

https://man.freebsd.org/cgi/man.cgi?query=dialog


Search for "flicker fusion rate" to learn a lot more about this.

That talks about the mechanics of visual perception. I'm discussing qualia, which I am far more confident crows share with me than does the particular subtype of Hacker News commenter who will with tiresome predictability and total lack of novelty turn up to press the footless insistence that crows could never.

Mine is 42 Hz according to a recent examination. Are high refresh rate monitors are wasted on this pair of eyes?

Our flicker fusion rate is different for the fovea and nearby central vision vs the peripheral vision.

The central vision is slower-response, higher-resolution, and of course color vision.

The peripheral vision is monochrome and has a much faster flicker-fusion, tuned to picking up motion in the periphery.

So, the same flicker rate that you never notice on a small monitor may flicker annoyingly on a large monitor. To check that a setup will not flicker for you, set it up in a darkish room, focus around 70°-100° to one side of the monitor so it is in your peripheral vision, and both look at one place and notice your periphery, and also move your focus quickly from one place to another and notice if the screen blurs like bright stationary objects or looks like a discontinuous blur (really easy to get that effect with fluorescent lights). Do it both left & right and towards the ceiling. If flicker shows up in these tests, it will still eventually bug you when looking directly at the screen, even if it isn't as noticeable because your focus is in the center of your vision.


No. Flicker fusion only happens when the same image is shown at the same position.

Something like a moving mouse cursor shows the same image at different positions. As an experiment, create a fullscreen image with the opposite color of your mouse cursor. Look at a fixed spot of this image, then rapidly move your mouse cursor across it. Rather than a moving image, you will see a bunch of copies of the cursor at fixed positions.

Similarly, track a rapidly moving cursor with your eyes. It will appear blurry, even though your eyes have no trouble sharply seeing an object moving at that speed in the natural world.

You can also try flashing an image for a very short amount of time. You'll be able to see and remember its content, even when it is being displayed for a period far shorter than flicker fusion would suggest you'd be able to see.


I don't know. Have you tried one? That's neither the rhetorical nor the dismissive response it may seem...

The mouse is very snappy compared to a 60 Hz display.

Just do a basic double blind test. get someone else to switch the hz a couple of times for you, and see if you can tell the difference. i would be surprised if you got anything less than a 100% success rate.

Dr Nyquist recommends double +1

And you didn't get married!?

Not OP, but I'm friends with crows. Imagine having to try to explain that...

Very intelligent birds.

"Baby, those body parts mean nothing to me! I love crows!"

Don't hate the player, baby.


They have a much stronger sense of propriety than most humans. So really do most animals other than us and perhaps some close relatives. I'm not actually sure that says anything in our favor.

Counterpoint: If I had to talk on the phone with the company instead of using text, I would choose a different company.

Text accomplishes the same thing but spread out over many hours instead of, like, 5 minutes. Phone call + summary email is so much more efficient.

You prefer the AI slop that pours out?


Yeah, I saw that... not quite the same... I used it for a bit but it's more like an agent that clings to a Github repo and deals with tickets up there, can't really test live on local, it just serves a different purpose.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: