pfdietz

7 ms·

181.
by pfdietz 2mo ago
Nevertheless, this is a demonstration that verification can produced apparently bug-free code.
182.
by pfdietz 2mo ago
Catapults store energy using elastic deformation, like a bow; counterweight trebuchets store energy using gravity.
183.
Three different papers pushed to ArXiv proving same 1986 conjecture; all use AI(twitter.com)
2 points by pfdietz 2mo ago|0 comments
184.
by pfdietz 2mo ago
> Ordinary testing using a few handpicked example Ah, but if you have specifications, you should have the ability to generate unlimited numbers of tests. Handpicked examples aren't needed. The great advance in testing with increa
185.
by pfdietz 2mo ago
Lean terms and programs have defined meanings, just like anything mathematical does. It sounds like you're asking something nebulous, like does it have a soul. Mass generation of conjectures and proofs/disproofs could AI to discov
186.
by pfdietz 2mo ago
Yes. Note that fuel rods don't move, so they would not "drop into the core". They can later be lifted out when the reactor is refueled but are fixed in place when the reactor is in operation.
187.
by pfdietz 2mo ago
So, if Google consciously throws books in the trash, that's ok, but if they scan them first, that's not ok? Or maybe this is just a thin veneer over anti-techbro antipathy. If destroying a book is such an evil, then isn't not
188.
by pfdietz 2mo ago
Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler. Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C co
189.
by pfdietz 2mo ago
> We didn't have enough compute back then. The problem here is that more compute also helps testing. So it's not clear verification will pull ahead over just doing more testing, especially if there's any manual part of
190.
by pfdietz 2mo ago
The material is doped by varying the overall oxidation state of the copper, which is balanced by the number of oxygen ions.
191.
by pfdietz 2mo ago
> Paradox is a statement that can't be proved true or false No it isn't. > execution of a Turing machine can't be expressed as a Gödel number Yes it can.
192.
by pfdietz 2mo ago
Obviously actual intelligence has an ineffable essential aspect, just like unicorn farts do.
193.
by pfdietz 2mo ago
> The entire point of writing proofs is for advancing human understanding. Proofs also enable AIs to direct search and generate knowledge. Verifiability is immensely useful for keeping AI grounded. One might imagine AI generating enormo
194.
by pfdietz 2mo ago
Your prissy outrage isn't a convincing argument that they are doing anything wrong. Books are lumps of cellulose carrying information. Destruction of excess copies is no more outrageous than discarding excess packets off the internet.
195.
by pfdietz 2mo ago
How is that a paradox? And how does that imply the correct argument I gave doesn't work? (It doesn't imply that.)
196.
by pfdietz 2mo ago
Your word salad is not even wrong. For example: > Gödel number encodes a paradox WTF do you mean by this?
197.
by pfdietz 2mo ago
You can also obtain incompleteness from the unsolvability of the halting problem, by noting that if every statement in (say) Peano arithmetic were provable, one could solve the halting problem. Encode a halting execution of a TM as an inte
198.
by pfdietz 2mo ago
Theory says radix sort on a set of strings runs in time linear in the sum of the sizes of the strings.
199.
by pfdietz 2mo ago
And 420 people can describe themselves as baked.
200.
by pfdietz 2mo ago
By "in practice" do you mean with one-implementation languages? If there's more than one implementation, there better be a standard, and it's risky to assume any behavior not specified in the standard will be shared by a
201.
by pfdietz 2mo ago
There is no need for an organized, unified project for life to spread across the galaxy, any more than there's a need for a unified effort for bacteria and fungi to consume some tasty organic matter, or for humans to have spread across
202.
by pfdietz 2mo ago
And puckish.
203.
by pfdietz 2mo ago
If I were saying we were definitely rare or unique, you'd have an argument. But I'm not doing that -- I'm saying it's a possibility that is consistent with evidence. The claim that life is common is different. For t
204.
by pfdietz 2mo ago
These companies have very low profit margins (as a fraction of cash flowing through them). They have strong incentive to keep costs down. What does stock price have to do with this? A high stock price can just mean there's relativel
205.
by pfdietz 2mo ago
Well, and also because of the "I've been told in Scheme you should do it this way, so by gum I'm going to do it this way!"
206.
by pfdietz 2mo ago
One place where this shows up is in parse trees. The grammar for a list of things may involve productions that look like list constructors. This, directly translated into a data structure, would give a very long chain of parse tree nodes
207.
by pfdietz 2mo ago
Even SBCL doesn't do TCO at all times. Compiling at (debug 3) means no TCO. Another related footgun is deep recursion of other kinds, for example when recursively traversing down lists. For long lists it's easy to exceed the sta
208.
by pfdietz 2mo ago
Lack of TCO is also a common footgun for Scheme programmers using Common Lisp.
209.
by pfdietz 2mo ago
This is an attitude that sets one up to be blindsided by developments. It's backward looking, not forward looking.
210.
by pfdietz 2mo ago
You confused $/kg with $/ton.

More ›