dwheeler

93 ms·

961.
by dwheeler 7y ago
> Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, b
962.
by dwheeler 7y ago
>> i found the foundations via set-theory unintuitive and a bit ackward to work with. > Type theories, especially dependent type theories a la Martin-Löf, are quite natural to work with (and) are easier to implement on a computer..
963.
by dwheeler 7y ago
"Prefix notation is a non-issue" is true for a tiny minority of software developers and mathematicians. The world has already spoken: infix is a minimum requirement for the vast majority of people doing math. Bignums, true ration
964.
by dwheeler 7y ago
Confirm, doesn't work for me on FF on Windows. And this is a challenge for a "new" format: if AV1 works on 90% of systems, and GIF works on 100%, then in many cases GIF is the clearly correct solution. Why would I throw away
965.
by dwheeler 7y ago
CSP could be better, but it's perfectly useful as it is. The problem is that too many people did things badly (using inline JavaScript), mixing up code and data. It's time-consuming to fix problems like that, but possible. Enab
966.
by dwheeler 7y ago
It may be a wise use if a security break-in would be a problem for your client. I am a big fan of restrictive CSP, but it's often hard to get there from an existing site. It's often better to do it in stages, e.g., when you work
967.
by dwheeler 8y ago
It's not like there was no oversight. As noted in the article, their boss was in on it, and "the rest of us leveraged our OldTuber status to approve the code review." so there was review. They short-circuited a number of the
968.
by dwheeler 8y ago
> Edit: this is exactly what a monopolizer looks like in action. One tactical move at a time, until they have full control of an adjacent layer in the value chain. In this case browsers. I think this was fundamentally different than a mo
969.
by dwheeler 8y ago
> I'm not that interesting; I don't have anything to show off; and inevitably it'll either become a chore or go out of date. I think it's a good idea to have a personal web site. If someone wants to find out more abo
970.
by dwheeler 8y ago
I would dearly love to have this. If it's controlled by software, then it is subvertible in a way that pure hardware solutions should be invulnerable to.
971.
by dwheeler 8y ago
GitHub, GitLab, Shopify, and many other sites use Rails. It's still a good choice for certain kinds of sites.
972.
by dwheeler 8y ago
I posted some ideas on how to reduce the risk of this kind of problem in the future. See: https://dwheeler.com/essays/bootstrap-sass-subversion.html
973.
by dwheeler 8y ago
That's also my understanding. My understanding is that these specifications were not developed in the open, and thus there was no opportunity for external scrutiny before they were ratified. It's exactly the same reason previous
974.
by dwheeler 8y ago
I think you are misunderstanding the phrase trade-off. A trade-off means that something is good for one thing, but not as good for something else. Your examples are exactly an example of a trade-off. A hammer is good at hammering nails, but
975.
by dwheeler 8y ago
> If everyone just focused on business value and ignored the technology aspects then nothing would've been invented. > There would be no Internet, Web, VR, ML, AI etc and we would all be writing assembler or using punch cards. Th
976.
by dwheeler 8y ago
In short: Pick the right tool for the job. Some projects need systems like React; some don't. A lot of projects do NOT need complex underlying systems - and some do. It's sad that "pick the right tool for the job" is
977.
by dwheeler 8y ago
"Projects could then submit for certification... who would do this certification, and how would they determine the criteria?" There's already something that takes a stab at this, the Linux Foundation's CII Best Practices
978.
by dwheeler 8y ago
> Some theorems have many different proofs that use different methods to prove the same theorem. These different proofs provide different perspectives that lead to a better understanding of the topic. Agreed, but there's no conflict
979.
by dwheeler 8y ago
> And rigor itself? A relatively modern requirement. Perhaps. I would argue that it is LONG overdue. > Moreover, math itself resists rigor in a fundamental way, as Godel showed us. This merely shows that some things cannot be prove
980.
by dwheeler 8y ago
I have done some, thanks for pointing to that page! Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice): http://us.met
981.
by dwheeler 8y ago
> Why do you insist mathematicians become programmers? No one is insisting that. We're insisting that proofs actually be correct, something that demonstrably cannot be done (to an adequate level) when we depend only on humans. Hum
982.
by dwheeler 8y ago
>> denying the legitimacy of computer-generated proofs protects their livelihood/careers. > While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. I t
983.
by dwheeler 8y ago
> I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect com
984.
by dwheeler 8y ago
My thanks to the original reporter of the vulnerability, and to the Rails folks for fixing it. I strongly recommend using at least one tool to help you know when a publicly known vulnerability is reported in a component you use. Then you ca
985.
by dwheeler 8y ago
I have added several examples of python3 programs that have exactly the same problems for exactly the same reasons. Hopefully that will clarify things.
986.
by dwheeler 8y ago
I have modified the article to show examples where the same problems happened in python3. Hopefully that will make it clear to people that this is not just a shell problem, and that writing everything in some other language does not solve t
987.
by dwheeler 8y ago
Short answer: No. The original "lint" was developed many decades ago. The problem is that C just doesn't provide enough type information to really do this properly. For example, there's no difference between "poin
988.
by dwheeler 8y ago
This is really promising work. However, it doesn't support free() at all; without free(), it seems less useful. It's not clear to me what supporting free() would involve; I'd love to hear comments.
989.
by dwheeler 8y ago
There is no way to enforce unified command line processing across all possible languages and all possible programs. Even if you did, how would you enforce knowing what a leading dash is? There's no way to tell the difference between a
990.
by dwheeler 8y ago
It is currently in my queue of things that I want to do. However, seriously making a Linux kernel module requires multi hour blocks of time that I have struggled to find. I hope to get back to it.

More ›