1,046 karma · joined August 15, 2021
Why is "many worlds" the most mathematically consistent? (I won't bother asking for the philosophical bit; I'm sure it's too long for an HN post.)
Christians: "We have faith supernatural selection at a cosmic level makes afterlife way more likely."
All times in seconds (lower is better)
benchmark Node.js Python 3 Py takes x times longer
==================================================================
regex-redux 5.06 1.34 ** Py3 is faster (PCRE C)
pidigits 1.14 1.16 0.02
reverse-complement 2.59 6.62 2.56
k-nucleotide 15.84 46.31 2.92
binary-trees 7.13 44.70 6.27
fasta 1.91 36.90 19.3
fannkuch-redux 11.31 341.45 30.19 (wut?)
mandelbrot 4.04 177.35 43.9 (srsly?)
n-body 8.42 541.34 64.3 (no numpy fortran cheat?)
spectral-norm 1.67 112.97 67.65 (Python for Science[TM])
Both ecosystems have billions invested by corporations worth trillions; bottomless money exists to make Python faster. So why isn't Python faster?
V8's tactics include dynamically watching which loops/calls get run more than (say) 10,000 times and then speculatively generating[2] native machine instructions on the assumption the types don't change ("yep, foo(a,b) is only called with a and b both float64, generate greased x86-64 fastpath"), but gracefully falling back if the types later do change ("our greased x86-64 'foo(float64,float64)' routine will be passed a string! Fall back to slowpath! Fall back!"). Why doesn't Python do this? Is it because Google recruited the only genius unobtainium experts who could write such a thing? Google is a massive Python user, too.
[1] https://benchmarksgame-team.pages.debian.net/benchmarksgame/...
[2] https://ponyfoo.com/articles/an-introduction-to-speculative-...
EDIT: HN commenter Jasper_ perhaps has the answer in another post[3]: "The current CPython maintainers believe that a JIT would be far too much complexity to maintain, and would drive away new contributors. I don't agree with their analysis; I would argue the bigger thing driving new contributors away is them actively doing so. People show up all the time with basic patches for things other language runtimes have been doing for 20+ years and get roasted alive for daring to suggest something as arcane as method dispatch caches. The horror!"
After so many years of endianness bugs in C/C++ code, it's perplexing that the web standards committee voted to put typed arrays in Javascript in such a way that exposes platform byte order to Javascript programmers who can't generally be expected to have low-level C/C++/ASM experience with memory layout issues:
function endianness () {
let u32arr = new Uint32Array([0x11223344]);
let u8arr = new Uint8Array(u32arr.buffer);
if (u8arr[0] === 0x44)
return 'Little Endian';
else if (u8arr[0] === 0x11)
return 'Big Endian';
else
return 'WTF (What a Terrible Failure)';
}
Anyone have a PDF link to a paper about this Fortran analyzer?
The expansion of the observable universe itself being apparently FTL is perhaps the most interesting. If we point the Hubble telescope (and soon JWST) towards opposite ends of the observable universe, we observe extreme redshift galaxies receding away from each other in opposite directions greater than twice lightspeed if we measure according to "distance in light years" from earth. But no photons or information from a galaxy at one side of our observable universe can be sent to a galaxy at the opposite end: they are receding away from each other too rapidly, these two galaxies exist Beyond the Cosmological Event Horizon relative to each other and are forever unknowable to each other, and thus causality is not violated.
An advanced alien race in galaxy A might be able to beam a message to earth before galaxy A vanishes Beyond the Cosmological Event Horizon within the next 100 million years earth-time, and likewise galaxy B might beam a message to earth within the next 100 million years earth-time, but earth can't relay the message from A to B or B to A because they have already forever receded from each other and will soon both likewise forever recede away from us.
- never talk to cops
- never read a patent
- never read proprietary source code
The patent system only benefits (1.) rich corporations that can afford the millions of dollars in lawyer fees to litigate patent claims, (2.) the lawyers that receive said fees.
def foo(bar, baz):
bar(baz)
...
grep -ri '\(foo\|bar\|baz\)' --include \*.py
So the earliest C compilers were under 5000 lines of C+asm:
https://github.com/mortdeus/legacy-cc
http://port70.net/~nsz/c/c89/c89-draft.txt
C doesn't need "defer" because C programmers have managed since the 1970s to implement operating systems, compilers, interpreters, editors, etc., just fine without it. Those who want a bigger C can use C++, this pond is big enough for two fish.
A great strength of C is that if you want more features you just go to a subset of C++, no need to add them to C. C++ is the big, ambitious, kitchen-sink language. When C++ exists we don't need to bloat C.
Fortran was originally carefully designed so that people who aren't compiler experts can generate very fast (and easily parallelized) code working with arrays the intuitive and obvious way. But later Fortran added OO and pointers making it much harder to auto-parallelize and avoid aliasing slowdown. Now that GPUs are rising it turns out that the original Fortran model of everything-is-array-or-scalar works really well for automatically offloading to the GPU. GPUs don't like method-lookup tables, nor do they like lambdas which are equivalent to stateful Objects with a single Apply method.
Scientists are moving to CUDA now, which on the GPU side deletes all these features that Fortran was bloated with. Now nVidia offers proprietary CUDA Fortran which is much more in the spirit of original Fortran, deleting OO and pointers for code that runs on GPU. If the ISO standards committee didn't ruin ISO Fortran for scientific computing by bloating it with trendy features we could all be running ISO Fortran automatically on CPUs and GPUs with identical code (or just a few pragmas) and not be locked in to proprietary nVidia CUDA.
But GPUs are now mainly used for crypto greed instead of science for finding cancer cures or making more aerodynamic aircraft so maybe it all doesn't matter anyway.
If they bumped 1200 MW to 1210 MW they'd have the 1.21 GW they need to operate a Flux Capacitor.
https://lisp.com.br/archive/ansi_cl_standard_draft_nice.pdf
The Java JVM was carefully designed to give identical results on all hosts for the Java platform unless you go out of your way to get nondeterminism or platform specific behavior (make the value of the number N depend on thread scheduling, or use JNI that assumes a platform byte order, etc.). C/C++/Rust allow undefined behavior if you shift a 64-bit int more than 64 bits, but Java on the JVM for example masks the lower 6 bits of a 64-bit shift ('& 0x3f') so that you get the same result on all CPUs rather than a CPU-dependent result:
https://docs.oracle.com/javase/specs/jls/se8/html/jls-15.html#jls-15.19
Clojure is a Lisp that runs on the JVM. I haven't personally used Clojure, but having done quite a bit of Common Lisp, Emacs Lisp, Scheme, etc., it looks to be very well designed and very well loved by its users, and using it could spare you from having to language lawyer the ANSI Common Lisp standard, as it seems to be more "try it and see" friendly.
I've been learning a lot about formal verification for C programs, how to truly make code that is bug free, and to do this you need to first make certain decisions about how you are going to formalize the language standard. E.g. will you assume that CHAR_BIT==8 or will you allow CHAR_BIT>=8 because the official ANSI/ISO C standard allows this even though all modern computers have CHAR_BIT==8? Then for any program you input to your verifier you must judge whether all its behavior is well-defined or if there is undefined behavior (arithmetic overflow, etc.).
There are quite good formal verification tools for Java, also, like JBMC and Krakatoa, and smaller Lisp languages are traditionally among the least tedious to formally verify (very simple semantics, unlike Common Lisp), but the time investment to learn these tools is enormous.
My Dear Dude, you are surely aware that computer editors are Religion among programmers, that vi vs. emacs, tabs vs. spaces, etc., have been fiercely debated for decades and will continue to be fiercely debated for decades to come. Thus, like all matters of politics and religion, if you are going to insult the Editor Religion of your fellow programmer and call it a gimmick, you might do well to at least accept the challenge when foul is cried and the gauntlet is thrown down demanding a scorable, quantifiable, objective, numerical measure of your performance claim that settles the question as fact rather than opinion.
But you would do better still to refrain from insults like 'gimmick', especially when the programmer whose favored multi-cursor feature you are insulting has demonstrated a deep interest in the history of computer editors, naming out ed/vi/vim/emacs/Sam/Acme/VSCodium, etc., and fully understands how to do ':%s/foo/bar/gc' in vim and the more powerful things documented by ':h :s' within vim and the even more powerful things yet in Acme involving the 'x' and 'X' commands but despite all this has found that multi-cursor can usually finish the edit before even half of that ':s///' command can be typed or a suitable regular expression mentally devised that gobbles the correct substrings on the correct lines without accidentally gobbling incorrect substrings on incorrect lines or incorrect substrings on correct lines or correct substrings on incorrect lines.
The original FORTRAN '57 did not even have SUBROUTINE, FUNCTION, CALL, etc., for implementing subroutines. Those came with FORTRAN II in 1958, which was the main language Kemeny's original BASIC was based on in the early 1960s, but Kemeny changed FORTRAN II's DO loop to the easier to remember 'FOR I = 1 TO 42 ...'.
Knuth designed his original 1960s MIX computer using just pencil and paper, designed it to be easy to run programs using just pencil and paper.
If you yourself could not build a rudimentary BASIC or cut-down FORTRAN using only the resources in your brain and a sheet of paper with a pencil, you might be spending too much time working with overcomplicated programming tools that do not bring joy to your life.
Here's a real example from real coding I was doing, then:
color.r = 42;
color.g = 42;
color.b = 42;
1. Alt-click after the two 42's I want to change
2. Ctrl-Backspace, type '255'
3. Done
1. Use '/42<RET>' or '?42<RET>' to search towards a 42 I want to change
2. Use 'n' or 'N' command to skip the 42 I don't want to change (possibly)
3. Use 'cw' followed by '255<ESC>' to change the first 42
4. Use 'n' or 'N' to get to the next 42, skipping the 42 I don't want to change
5. Use '.' to repeat the 'cw255<ESC>'
1. Use ':%s/= 42/= 255/gc' to query replace the right occurrences
2. Answer 'y' or 'n' for each occurrence
3. Still requires more keystrokes, time, and thought than VSCodium
https://en.wikipedia.org/wiki/Magnetic-core_memory
Fabrice Bellard's minimalist but complete quickjs.c Javascript interpreter is presently about 54,000 lines of C:
https://github.com/bellard/quickjs/blob/master/quickjs.c
So here's an editing task. Given the following in your editing buffer,
signed char foo;
/* ... 10 more lines ... */
unsigned short bar;
/* ... 10 more lines ... */
const char *const s = "Dennis Ritchie little-loved 'const'.";
1. delete 'signed' from signed char foo
2. delete 'short' from unsigned short bar
3. delete the two occurrences of 'const' from 'const char * const s'
1. Alt-click just past the end of each of the 4 strings to be deleted.
2. Ctrl-Backspace.
3. Done.
1. Three keyboard keys total (Ctrl, Alt, Backspace), each pressed and released once.
2. Four mouse clicks total, plus four target aiming tasks for these clicks.
This sequence requires zero thought or planning prior to execution.
I want to see the keyboard keystroke count for your best vim sequence, which will require a pause to plan out prior to execution, whatever you come up with.
> This might be because I don't work from a desktop and use a trackpoint, or maybe because when I do use a desktop I use a trackball.
Multiple peer-reviewed human-computer interaction studies have shown that for a broad range of pointing and editing tasks the mouse is faster than touchpads, trackpoint nipples, trackballs, and pens. (I do use a pen occasionally and if not for the pressure/tilt sensitivity it would be mostly pointless.) There's no need to dig into the literature because you can just try it yourself: next time you have both a mouse and your trackpoint/trackball handy try benchmarking your performance at,
https://humanbenchmark.com/tests/aim
Also try
https://aimtrainer.io/
If you do not personally like mice or mouse driven multiple-cursors that's cool, enjoying the journey is often more important than getting to the destination as fast as possible.
But I do claim that if and when text editing competitions for prize money are held, those who use mouse-driven multiple selection will be at a decisive competitive advantage over those who don't. This is just a claim which I cannot prove until such competitions are held. And, again, if a mouse makes you less happy than something slower, then the tortoise beats the hare, so to speak.
Pianists can rapidly move their hands to 100% accurately strike keys more than a foot away at blink-of-the-eye speed because they practice, and master mouse users can flick their hand from keyboard to mouse to keyboard again at blink-of-the-eye speed if they practice. Anchoring at the keyboard is not the fastest way to edit text.
There needs to be a text editing competition organized with prize money. Then shall all the world see that mouse users best the Rodentless in battle.
If I need to double-backspace five different caret positions visible on screen, I can Ctrl-click (or Alt-click) to set multiple cursors faster than a master vimmer's brain can devise a suitable ':[x,y]s/.../.../g' command to accomplish the same thing. I know this because I've used vim more than 20 years, and I also learned ed's and sam's editing languages used by the original Unix gods. The Unix gods switched to the Sam editor in the early 1980s which is a bit like a mouse-oriented re-imagining of vi. Then some switched to Plan 9's Acme in the 1990s, which retains Sam's editing language. The Sam/Acme editing language is not line-oriented like ed/vi/vim, e.g. ':#3,#42' selects character 3 through 42 regardless of how many newlines are between char 3 and 42 and does not select to the beginning of the line before char 3 nor to the end of the line after char 42. You can also do ':/re1/,/re2/' and unlike vim this won't grab to the beginning of line before /re1/, etc. Acme doesn't have multiple cursors though and needs some TLC, it doesn't talk to an X server efficiently and draw pixels efficiently because it's based on Plan 9's drawterm. VSCodium does everything I need but is ultra-bloated and I'd love lighter weight.
1. How well do you handle the mouse in xterm? Vim actually has fantastic mouse support in xterm (:set mouse=a), e.g. you can use focus-follows-mouse scrollwheel to scroll individual split content panes, drag click to resize the split dividers, etc. (Although, last time I tried under WSL with the old-school win-console, vim's focus-follow-mouse scrollwheel scrolling didn't work there whereas emacs did work (with xterm-mouse-mode)).
2. Can you handle multiple cursors gracefully (vim-visual-multi) with the mouse like VSCodium? Emacs doesn't have a non-buggy multi-cursor mode and I gave up on achieving this with Emacs. I just use VSCodium now, which means allocating over 300MB of system RAM and gigabytes of dedicated graphics VRAM for its 'HW accelerated' rendering that decelerates all other HW graphics rendering on my machine.
SPARK does not allow doubly linked lists:
https://blog.adacore.com/pointer-based-data-structures-in-sp...
For example, singly-linked lists and trees are supported whereas
doubly-linked lists are not.
However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.
AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:
https://github.com/AdaCore/why3
And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:
https://github.com/gcc-mirror/gcc/tree/master/gcc/config
Compare with CompCert, the formally verified C compiler:
https://github.com/AbsInt/CompCert
Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:
Coq has been used to formally verify a large body of classical mathematics. Coq can 'understand' what a prime number is and can be used to prove that there are infinitely many primes, can prove that sqrt(2) is irrational, etc. Coq can prove a recursive solver for the Towers of Hanoi actually solves the problem, etc. And thus Coq can prove a C program to solve the Towers of Hanoi correctly solves the problem, because Coq can reason about C programs.
I've been slowly working through the Software Foundations series on using Coq/Gallina:
https://softwarefoundations.cis.upenn.edu/
Another poster mentioned CBMC which I just started playing with. It is much less powerful than Frama-C, there isn't the ACSL specification capability and theorem proving, but it is much more automatic and much faster to get started with. For many cases if I just want to verify that a certain C file frees all its mallocs, doesn't have out-of-bounds accesses, and that all obviously bounded loops terminate, CBMC is much easier. Also, like Frama-C, it converts C functions into "goto programs" (removes the syntactic sugar of 'for' and 'while' loops to obtain a more pure Control-Flow-Graph (CFG)) for certain forms of analysis, and when I first encountered this in Frama-C there was no explanation why, whereas the manual for CBMC actually has an excellent gentle introduction:
CBMC can also be used for programs with unbounded loops. In this
case, CBMC is used for bug hunting only; CBMC does not attempt to
find all bugs.
However, having now gone through the CBMC manual, it appears to be much faster and easier to use for my own limited purposes than Frama-C. I don't need a sledgehammer to swat flies. I also like that the installation procedure on my machine was simply,
$ sudo apt install cbmc