ukj

57 ms·

511.
by ukj 7y ago
That's fair. I actually find Coq rather painful to use. It gives me the distinct impression that it has been designed/implemented by somebody who has never written human-computer interfaces before. When it comes to adapting humans
512.
by ukj 7y ago
But it's once-off work. Thereafter the computers can take over.
513.
by ukj 7y ago
Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project. [1] https://en.wikipedia.org/wiki/Coq [2] https://github.com/
514.
by ukj 7y ago
I did drop out. Learning is important. College is not the only way to learn. I acquire the knowledge necessary to accomplish my goals. I wouldn't hire; work with; or work for somebody who doesn't know how to manage the risk of T
515.
by ukj 7y ago
Defining the problem is half the solution ;)
516.
by ukj 7y ago
The reason I re-invent wheels is because I don't know the idiom I need to Google for. I know what I need. I don't know what it's called in English. It's faster to re-implement it than to learn the vocabulary.
517.
by ukj 7y ago
Has your judgment ever led you to conclude that something ought to be said and it's the appropriate thing to say, and then choosing not to say it anyway because you can't predict the response? I do that a lot. You could trivially
518.
by ukj 7y ago
Yeah, I've been watching the vote-count on this post. It's quite... erratic to say the least. It re-bounded from the negatives. Many angry down-voters bashing that [-] button only making my point.
519.
by ukj 7y ago
Statistically and predominantly that is my experience too, but in risk management you don't count your wins - you count your losses. It's not the 99 times when your parachute opens that you stress about. It's the other 1%. (M
520.
by ukj 7y ago
I am afraid to be mis-interpreted as hateful or bigoted, and have to spend an inordinate amount of time/effort either choosing my words for my audience (which is really hard on the internet with such a broad audience) or correcting kne
521.
by ukj 7y ago
I am a master at being 'indistractable' - my brain-CPU does not support interrupts. P.S my manager calls me 'uncooperative'.
522.
by ukj 7y ago
There is an interesting question to ask here. Do you learn more effectively by reading or by interacting? My bias is towards the latter. Real-time communication offers an opportunity for error detection/error correction in transmission
523.
by ukj 7y ago
It was also obvious from the essay that his Mathematical nihilism didn't extend to computation. So it kind of begs the question: What does Mathematics mean to a Computer Scientist? Least we forget that Ed Nelson was a strong proponent
524.
by ukj 7y ago
To call him a nihilist based on his views of Mathematics is a bit too reductionist, I think? All Mathematicians are human, not all humans are Mathematicians. Humans look for (and find) meaning wherever they can.
525.
by ukj 7y ago
Elsewhere, Nelson has stated that despite the labels Mathematicians use to describe themselves (Platonist, Formalists, Intuitionist) they still seem to have the uncanny ability to agree on the correctness of any particular piece of work, de
526.
Confessions of an Apostate Mathematician [pdf](web.math.princeton.edu)
3 points by ukj 7y ago|6 comments
527.
by ukj 7y ago
On-point. Exponentiation is not like multiplication because it's not associative. (2^3)^4 != 2^(3^4)
528.
by ukj 7y ago
Sure. Total functional programming (provably terminating code) comes at the cost of Turing-completeness. The choice exists. https://en.wikipedia.org/wiki/Total_functional_programming Observe though that BNF is just a n
529.
by ukj 7y ago
Curry-Howard isomorphism. Proving that a sentences are “well-formed” is the same as implementing an algorithm which takes a string and returns a Boolean. You can call this function “is_well_formed?” I await your proof in the regular languag
530.
by ukj 7y ago
Well, this looks like abuse of Cunningham's law, but I'll bite. It is a general rule that general rules have exceptions. And you have (incorrectly) asserted that this is not an exception. Q.E.D Even the most powerful languages (Ty
531.
by ukj 7y ago
So we agree then that when the system says "I am free of errors", some (most?) of the time it's a lie ? ;) All models are wrong - some are useful.
532.
by ukj 7y ago
I have already done that, what I am unsure of is how to go about convincing you. With compilers - I just fix the bug myself. With humans, I have to convince the human to self-correct. Common problem in distributed systems that - leader elec
533.
by ukj 7y ago
Are you sure you aren't mistaken? :-)
534.
by ukj 7y ago
All of them. "Type-0 grammars include all formal grammars. They generate exactly all languages that can be recognized by a Turing machine."
535.
by ukj 7y ago
Indeed. Type 0 Grammars are the most powerful grammars we have. https://en.wikipedia.org/wiki/Chomsky_hierarchy#Type-0_gramm... In this type of grammar Godel's incompleteness theorem is equivalent to the Halting p
536.
by ukj 7y ago
You are axiomatically assuming that the proposition "V determines well-formedness of any regular expressions" to be true. I am asking you to prove that. Constructively.
537.
by ukj 7y ago
> You seem to be mistaking validating a program's source with the question of whether it performs its intended purpose. In general, that is a useful distinction to make, but you forgot about the edge case where the distinction is me
538.
by ukj 7y ago
Precisely, but as far as a compiler/interpreter is concerned syntax is semantics. You can't codify moral judgments.
539.
by ukj 7y ago
The "liar" is saying that the Essay is free of errors. (To the best of the "liar's" ability to detect them). The liar's knowledge is incomplete. https://en.wikipedia.org/wiki/G%C3%B6del%27s
540.
by ukj 7y ago
So what you have to trust is that the spec doesn't produce lies ? ;) FYI. I am just having some philosophical fun with GIGO. Ultimately, computers are just instruments which amplify human intention, it's not the computers's j

More ›