User: nx2059

Not to be overly critical...

On: Donald Knuth On NPR

But I just wish he would do all his math in some kind of machine checked formal logic, it would make things easier to follow in his books. I know that people say that there are too many steps when you try do do a proof in formal logic, but we've come a long way, and most LCF based interactive provers, can do a lot of the grungy work for you, so you will still have the outline of the proof available. For example...

- val thm1 = PROVE [] ``~~A:bool = A``;
Meson search level: ....
> val thm1 = |- ~~A = A : thm

- val trm1 = ``x:bool``;
> val trm1 = ``x`` : term

- val trmTemplate = ``x /\ T = F``;
> val trmTemplate = ``x /\ T = F`` : term

- val thm = ASSUME ``~~A /\ T = F``;
> val thm = [.] |- ~~A /\ T = F : thm

- val result = SUBST [ trm1 |-> thm1 ] trmTemplate thm;
> val result = [.] |- A /\ T = F : thm

- show_assums := true;
> val it = () : unit

- result;
> val it = [~~A /\ T = F] |- A /\ T = F : thm

This might not be the best example (it's all I had at the moment) but as you can see in the first step, HOL proved ~~A = A, an obvious theorem that I couldn't find quickly in the library. HOL did this almost instantaneously, and routinely makes me look like a fool, proving stuff that will take me a half an hour in the blink of an eye. The user interfaces are a bit dated, but they have great potential for improvement.

Re:We're winning, let's change tactics

On: OSS Unix: Dividing & Conquering Itself

'll stay exactly where I am-- a Microsoft customer.

Slight correction. To Microsoft, end-users are not customers, they are consumers. Linux end-users tend to be participants, wherever they can.

The irony here is that you are insulting him.

Re:Better have something inline

On: When Should You Quit Your Job?

Am I a fool for giving up steady work and good pay?

Yes. Don't ever quite (read it twice) unless you have something else in line.

well, if your that stallmanish about your software, then who are we to argue with you? I quit (or rather was fired for telling my boss I didn't want her BS) my last job because my employeer wasn't paying me overtime, working me and my (firends) coworkers excessive hours, treating the office staff like shit when I knew they couldn't do their jobs until the reports were fixed. That and the owner consistently lied to customers (sorry "bent the truth"). There's an old saying, "If your not part of the solution, then you're part of the problem" I definiately felt like I was part of the problem, and nothing was being fixed, only one half-assed soultion pasted on another. So here I am 1 year later, still unemployed. I was ready to end up starving on the street if it came to that (We all die someday, why fear it?). But at least now I can do stuff like work & volunteer for orginizations I believe in, Instead of working my ass off to fill some fool's pocket.