dwheeler

76 ms·

841.
by dwheeler 7y ago
I've since discovered that the latest Forth standard, Forth-2012, includes an optional set of Forth words to support local variables. Gory details here (warning, spec-ese): http://forth-standard.org/standard/locals
842.
by dwheeler 7y ago
The problem with using global variables (like this) is that it's not thread-safe. Many Forth systems supported multi-threading (each thread gets its own pair of stacks), even on resource-constrained systems. If you're going to ha
843.
by dwheeler 7y ago
Many Forth developers do not like using named parameters AKA local variables. That said, they certainly exist, so if that is your only objection to Forth then there are easy ways to solve it. See, for example, http://zedcode.blog
844.
by dwheeler 7y ago
Forth is truly amazing in terms of what you can do with very little RAM and CPU power. It is quite possible to have a working interactive development environment and production implementation in only 4-8 kibibytes of RAM. In the world of sm
845.
by dwheeler 7y ago
Demo game: https://m.youtube.com/watch?v=qKcZwPb7C3k All death animations (Amiga): https://m.youtube.com/watch?v=iSnAiXKU7h8
846.
by dwheeler 7y ago
I did not have that problem, but I'm sure others do. I think the long-term solution is to make it clear that that is a gdpr violation, there is no reason that an unrelated third-party should get that information. Once people start gett
847.
by dwheeler 7y ago
It is quite possible to responsibly implement Facebook "like" buttons on your own pages without violating your users' privacy. I wish more people would do it. I suspect that including Facebook like Pages the way Facebook want
848.
by dwheeler 7y ago
There are fundamental differences between Stadia and Steam: 1. If Steam shuts down, Valve shuts down. If Stadia shuts down... Google is doing just fine. 2. What Stadia is attempting to do is much more technically challenging, and I'
849.
by dwheeler 7y ago
LibreOffice does let you create editable PDFs. They do this with a very elegant solution, they embed the Open document format within the PDF. This takes very little additional space, because the Open document format is compressed. I think t
850.
by dwheeler 7y ago
Cool! Thanks for the link!!
851.
by dwheeler 7y ago
It's a decent technique to check on compilers, but it's older than that. Arial Faigon discusses that approach in an undated blog post: http://www.yendor.com/testing/#compiler I don't know the date, but I
852.
by dwheeler 7y ago
I like the idea of having some standardized way of noting that. The indicator would have to be short and clear. Any ideas? Maybe "Music-only audio"?
853.
by dwheeler 7y ago
> Hmm, why do you recommend adding music? For the human. Videos are way more interesting to most people if there's an audio track of some kind. Anyone who doesn't like the sound can mute it. Less processing really isn't
854.
by dwheeler 7y ago
Gource is a really cool visualization tool. Here's a Gource visualization of development of the Python programming language (C Python implementation, aka CPython): https://www.youtube.com/watch?v=cNBtDstOTmA Here&#x27
855.
by dwheeler 7y ago
Gource is a really cool visualization tool, and although it's originally intended to show software development over time, it's useful for showing other community works over time. Here is a visualization of the development of set.m
856.
by dwheeler 7y ago
For a personal domain, own your own domain or be owned by someone else.
857.
by dwheeler 7y ago
I am skeptical that he will succeed, but I am happy that he will try. Carmack is smart, and we need smart people to try hard things.
858.
by dwheeler 7y ago
Modern logic and set theory meets some of the requirements of this. At the time, he did not have for-all, exists, and so on. Leibnitz himself created some proofs with the limited logic of his day. Nowadays much more can be done. It's n
859.
by dwheeler 7y ago
That certainly happened, but as far as I can tell they stopped that years ago. It hurt their reputation immensely, though.
860.
by dwheeler 7y ago
Computers can directly prove some theorems today, and in other cases there are various interactive provers that let humans and computers work together to find formal proofs. In some systems using computers can give much better confidence
861.
by dwheeler 7y ago
Intel/Siemens had a joint venture developing the BiiN hardware. The operating system, applications, development tools, and so on were written exclusively in Ada. However, a lot of that software fully worked on that particular chip, so
862.
by dwheeler 7y ago
4os was an operating system written in Forth. It was discussed on Hacker News in 2016: https://news.ycombinator.com/item?id=12709802 In many ways many Forth systems were simultaneously the programming language and the oper
863.
by dwheeler 7y ago
If you're interested in the main book on Metamath, it is "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler. You can get the hardcover here: http://www.lulu.com/sh
864.
by dwheeler 7y ago
FYI, the current publicly-available code for Metamath Zero is here: https://github.com/digama0/mm0
865.
by dwheeler 7y ago
> Logically it is a single proof, but technically it consists of quite a few theorems and lemmas, so this is not a valid comparison. I think it's 100% valid, indeed, the Metamath and/or Metamath Zero verifiers are verifying muc
866.
by dwheeler 7y ago
The 25 minute value is only the time to verify a single Coq proof. I'm measuring the time to verify ALL proofs of an entire system. The Metamath Rust verifier normally verifies 23,000+ proofs at a time. The actual verification time is
867.
by dwheeler 7y ago
This is really interesting work. I like this quote: "sometimes, performance is about more than just getting work done a little faster. When something takes a lot less time, it changes the way you interact with the computer. A process t
868.
by dwheeler 7y ago
It doesn't even need to use machine learning. I have written several analyses of metamath databases to look for common patterns, and then recommend definitions or theorems to simplify things. If some expression is repeatedly used over
869.
by dwheeler 7y ago
Perl 6 is really a different language from Perl 5, so I think the new name is what should have happened from the beginning. But I basically agree with you that using the name "Perl 6" for Raku led to most people abandoning Perl 5.
870.
by dwheeler 7y ago
There are other factors not mentioned in this article. First, most technologies are challenging to use and expensive at first. There are often related technologies that are required to make the first technology actually be useful. For examp

More ›