HNHacker News
TopNewBestAskShowJobs

dandotway

1,046 karma · joined August 15, 2021

submissionscomments
dandotway··on Why the C Language Will Never Stop You from Making Mistakes
"Big" software is mostly not difficult algorithms, but writing boilerplate glue code that connects the inputs and outputs of algorithms/functions that are usually written by someone else. Frama-C can definitely verify the boilerplate for "big" software, this is actually easier than verifying data structures and algorithms, which requires knowing the key property to get the prover to see that the algorithm always makes progress toward a solution. Once you have the contracts set up for calling a function, Frama-C will enforce that the contract is always met.

The CompCert verified C compiler is "big" software, but not actually written in C, rather OCaml and Coq/Gallina.

dandotway··on Why the C Language Will Never Stop You from Making Mistakes
And if cancer kills millions every year and successful treatments are expensive and tedious, maybe someone can come up with a cure to cancer that is not expensive and not tedious. It's a hard problem to solve, but a lot of smart people are working on that problem, too.
dandotway··on Why the C Language Will Never Stop You from Making Mistakes
> You test all possible values

Which is not feasible if there are, say 2^128 or more possible values. CBMC is a model checker, which is very useful for many problems that can be brute-forced but not the same thing as the correct-by-construction approach of Frama-C style formal methods, which deductively verifies that code works on all possible cases, even all conceivable edge cases, without having to exhaustively test all cases.

dandotway··on Why the C Language Will Never Stop You from Making Mistakes
Yes, Frama-C uses a plugin architecture, and there are plugins to verify all kinds of things, including functional correctness. The Frama-C tutorials page,

https://frama-c.com/html/tutorials.html

Has a link to the ACSL-by-example PDF which gives examples of creating in C various C++ STL inspired data structures and routines:

https://github.com/fraunhoferfokus/acsl-by-example/blob/mast...

Also, it is less effort to write bug-free code in OCaml than C. The Coq/Gallina proof assistant even has an OCaml-extraction (and also Haskell-extraction) feature where you extract runnable code from a formally verified algorithm in the Gallina specification language. (It's generally easier to proof theorems about code in the theorem prover itself, go figure.) Most of these C verification tools are written in OCaml, not C, with varying levels of assistance from Coq/Gallina.

The main reason the functional languages make it easier is because you generally execute side-effect free functions on data structures to give them the mathematical property you want. For example, you execute a lexicographical sort function on a list of strings and then the strings in the list all satisfy the mathematical property of a total ordering. You don't have to do any reasoning about the "in-between state" where pointers under the hood are being manipulated, and you don't have to add pre-conditions and post-conditions about the global environment if the code is side effect free and does not access non-local memory.

dandotway··on Why the C Language Will Never Stop You from Making Mistakes
Frama-C doesn't need to know anything about the target arch. It guarantees no undefined / implementation defined behavior on all architectures. You have to prove your code does not cause overflow/underflow (or accounts for it) if you add two integers or cast a uint32_t to an int32_t, etc. Very tedious, but it can and is being done.

CompCert, the formally verified C compiler, is a separate thing from Frama-C, but currently supports x86, ARM, RISC-V, and PowerPC. (CompCert is actually mostly programmed in OCaml and the Coq/Gallina proof assistant.) CompCert guarantees that a correct ISO C program (no undefined or implementation defined behavior) is translated into an assembler program with the same semantics, i.e. an assembler program that computes the same results as the C source program. So CompCert for each supported architecture needs a formal semantics for any CPU instructions it generates. CompCert is an optimizing compiler and the optimizer accounts for the delay between when an instruction is issued and when the result is ready, accounts for pipelining and all that if that is what you are asking.

But to write verified C programs you don't need to worry about instruction re-ordering happening lower down changing the meaning of your program and all that. That's a deeper layer of the onion, and, as Bjarne Stroustrup said, each time you peel a layer of the onion you cry more.

dandotway··on Why the C Language Will Never Stop You from Making Mistakes
Frama-C allows writing formally verified bug-free C. It is certainly tedious though; you essentially have to write two versions of every function: (1.) the actual C code for the function; (2.) a declarative formal specification of what the function does in ACSL (ANSI C Specification Language), stating all relevant pre-conditions that must be met prior to calling the function, and all relevant post-conditions that hold after the function runs. Then you have to add annotations to computation steps in the function code proving it causes the post-conditions to hold if the pre-conditions hold.

Nevertheless, it is extremely powerful because it can prove the correctness of arbitrary heap manipulation algorithms (lists, trees, graphs). You can formally prove complicated C pointer manipulations are correct that cannot be expressed in 'safe Rust'. There is also the CompCert formally verified C compiler.

I've also studied Ada/Spark's formal verification abilities and C is way ahead here. C is also way ahead of C++ because C has far fewer complicated semantic rules that need to be formalized before they can be analyzed. Even parsing C++ is an enormous task.

In the coming decades as the automation and ease-of-use of formal verification tools improves, I think C may well end up being the best choice for security-critical and correctness-critical systems programming. With current tools it is already ahead of Ada, C++, and Rust.

https://frama-c.com/

dandotway··on The Story of the Game Genie, a Cheat Device Nintendo Tried (and Failed) to Kill
Interesting legal tidbits:

  They even had Shigeru Miyamoto in court - he came to San Francisco.
  They were saying that because the player was plugging in the
  interface and making Mario jump higher, the player was making a
  derivative work, and we were helping him infringe copyright. In the
  end, the judge said it was not permanently changed when you
  unplugged it, and for a derivative work to exist it has to be
  permanent.
  
  [...] Some of the team's tactics were quite interesting,
  highlighting the hypocrisy of Nintendo, as Menzies explains. "I
  helped with the lawsuit by creating non-Game Genie codes that could
  be entered into an official Nintendo game's own password system and
  would crash it, cause graphical corruption, weird behaviour, and so
  on. Basically all of the things that Nintendo's lawsuit accused
  Game Genie of doing, so we could say to the judge 'look, this isn't
  anything to do with us, Nintendo's games do this on their own, it's
  just how video games work'."
dandotway··on Facebook exec blames society for COVID misinformation
Many word have trick. Make see different than few word.
dandotway··on Facebook exec blames society for COVID misinformation
Homo Sapiens have been murdering each other on this planet for at least 10,000 to 100,000 years, and have only used burning-powder projectile launch tubes for roughly the past 1000 years. (Poison darts launched from a blowgun are a more ancient form of killing tube.)

When convenient projectile launching killing tubes aren't available, Homo Sapiens will rapidly revert to 10,000+ year old murder methods, and thus a husband inflamed with murder-rage who just learned his wife's ovaries have been voluntarily fertilized by another man's semen will not infrequently use punches or a nearby blunt object (hammer or rock) to fracture her skull and destroy her brain function, or use his hands to crush her windpipe, or bleed her out with a knife. This has been happening essentially every year for at least the past 10,000 years. If his wife had been armed with a handheld projectile launching killing tube she could have defended herself, but women frequently don't carry projectile tubes and frequently vote for restricting access to projectile tubes, because projectile tubes are loud and scary and make them feel unsafe.

dandotway··on Magma: A Dependently-Typed Language
I've tried SPARK. Compared to Frama-C, SPARK is not as powerful. Frama-C can prove the correctness of arbitrary heap manipulation algorithms. SPARK can handle singly linked lists but not doubly linked lists (last I checked).

Although, usually the people who use SPARK use it because it is certified for their industry (such as aerospace).

dandotway··on Tell HN: GitHub is down again
Laws need teeth to be enforced. It used to be illegal to harbor runaway slaves, or to be a Catholic priest in Protestant England. So people built cleverly hidden Priest Holes[1] in houses to hide. But you can't really build the equivalent of a Priest Hole within Github, because Github is not your house, but rather your lord's castle.

[1] https://en.wikipedia.org/wiki/Priest_hole

dandotway··on Tell HN: GitHub is down again
In the 1970s-80s we managed with email lists and tarballs on multiple mirrors. Git itself decentralizes source control, and yet we all want to use single-point-of-failure Github.

Anyone remember when Github took down youtube-dl?

I wonder how much Big Brother data Microsoft is gathering on Github developers. "Oh, as part of our hiring process, just like we scan your FB and Twitter, we also scan your Github activity to evaluate your performance as best as our machine learning overlords can assess it. Do you create Github projects and then abandon them when unfixed issues accumulate? Our algorithm thinks you're a bad hire."

dandotway··on Magma: A Dependently-Typed Language
The boxer Mike Tyson put it well, "Everyone has a plan until they get punched in the mouth."

I discovered Coq and OCaml by way of the Frama-C framework for formally verifying C programs. This is a system that works today. It does need to be made lower friction to install and get started with, but the author of this repo bashes on Coq and its researchers as if he were a young firebrand politician taking on Big Tobacco and Big Pharma. He even says, 'And let's be honest, the name "Coq" is just terrible.'

I wish him well on his crusade against Big Coq.

dandotway··on Historically Black College grads average $927,000 more throughout career
https://archive.ph/vZ4cX

Summary: For moving blacks from poverty to the middle class, nothing outperforms Historically Black Colleges and Universities (HBCUs).

Key takeaways:

- "The unique contribution of this study is to examine students from the bottom two quintiles of household income ($46,000 or less)—and then find out how many later make it into the third quintile or above."

- "While HBCUs educate only 10% of all African-American college students, HBCU grads account for 80% of black judges, 50% of black doctors and 50% of black lawyers."

- "An HBCU graduate working full-time throughout his career will earn $927,000 more when compared to non-college goers and black students at non-HBCUs."

dandotway··on GC progress from JDK 8 to JDK 17
So I just tried to set up MonoGame as a result of this thread, but with a twist: only use non-Microsoft servers as sources, to see if it really is 'open source'.

It's impossible.

I just spent 30 minutes trying to find a single non-Microsoft mirror for the .NET Core dependency. If MonoGame is your Spice Melange then Microsoft's servers are the planet Arrakis, the only source in the known universe.

On Ubuntu you need to add a Microsoft server as a repo, you can't just "apt-get install dotnet-sdk-6.0".

So, yeah, MonoGame is not for me. I'll stick with Godot or SDL2.

dandotway··on GC progress from JDK 8 to JDK 17
Great catch! The Wikipedia article for MonoGame lists Hades, but is evidently wrong. Hades used The Forge for graphics. Ctrl/Cmd-F "Hades" on the Github page has some info:

https://github.com/ConfettiFX/The-Forge

The Forge is graphics only; audio, input, etc., have to be handled by something else and Hades used a custom C++ engine apparently.

dandotway··on GC progress from JDK 8 to JDK 17
So I just spent some time looking at all of these you listed. With the exception of libGDX they are all essentially desktop-only (Win/Mac/Linux).

LibGDX appears to support iOS/Android and HTML5 desktop browsers, but not consoles (Switch/PS/Xbox).

dandotway··on GC progress from JDK 8 to JDK 17
Good point, the Debian Benchmarks Game for example shows C# matching or considerably beating Java at everything except the binary trees benchmark which stresses GC/mempool performance.

https://benchmarksgame-team.pages.debian.net/benchmarksgame/...

I haven't tried C#/MonoGame yet but all this discussion is considerably warming me up to it. The recent extremely successful indie game Hades was made with MonoGame.

Microsoft in typical MS fashion makes MonoGame higher friction if you aren't using a Windows box for development with MSBuild. On Linux it appears you need to use Wine to run DirectX effect compilation, though once compiled it works on OpenGL backends:

https://docs.monogame.net/articles/getting_started/1_setting...

dandotway··on GC progress from JDK 8 to JDK 17
I love functional languages but is anyone actually using Haskell to develop for Nintendo Switch and PlayStation? Can you use Haskell on the Nintendo Switch to access a robust audio mixer stack?

F# can be used with C#/MonoGame which seems to run well everywhere so that's one route to functional programming gamedev. Another route appears to be to use SDL2 with a functional language that supports ANSI C bytecode runtime fallback. E.g. OCaml has a bytecode compiler and an ocamlrun runtime that can be compiled with an ANSI C compiler. But I don't know what the GC latency guarantees are for the bytecode runtime. OCaml's native low latency GC benefits from Jane Street's contributions because Jane Street uses OCaml for high frequency trading. But bytecode OCaml running on Nintendo Switch isn't the same thing as native Linux OCaml.

dandotway··on GC progress from JDK 8 to JDK 17
It sounds very nice but if more than half an indie game's revenue comes from Nintendo Switch then you need a low friction way to get your .java files running there. You also need a proven audio mixer stack so you can load background_music.mp3 and play bang.wav and boom.wav without any popping or leaks. Right now Java seems sort of iffy on consoles, as in, you could maybe spend a ton of time and/or money to get an effort like GraalVM production-grade working there, but no one has bothered to do it yet. It seems to be much lower friction to just use C#/MonoGame, or SDL2 with your scripting language of choice that compiles with a C/C++ compiler, or a proven game engine.
dandotway··on GC progress from JDK 8 to JDK 17
As Java is generally the fastest GC'd language, what's the current state of Java gamedev?

Once upon a time, this indie Java game called Minecraft became the most successful game of all time.

But from the few minutes of research I just did, Java cannot be deployed to many commercially important systems

  - Nintendo Switch
  - PlayStation
  - iOS
It appears Java is only still viable for Windows and Android, and the 1% Linux desktop market.

There used to be the GCJ project which would in theory let you run Java anywhere you had a C/C++ compiler, but Oracle's litigiousness killed that because the Java[TM] "platform" must run the official Java[TM] bytecode.

It appears C# via Monogame lets you deploy to all desktops (Win/Mac/Linux), mobiles (iOS/Android), and consoles (PS/Switch/Xbox). So ironically C# seems to now be the "write once, run anywhere" fulfillment of the original Java promise.

[EDIT: grammar.]

dandotway··on Go does not need a Java-style GC
+1 Not bad, your simple pool improved performance from about 10.9 secs to 1.4 secs on my laptop here. However, it does break the stated rules for the benchmark.[1] The Java version doesn't use a pool and doesn't change Tree pointers into ints as your version does. The C/C++/Rust versions are required to use a "library memory pool." The rules state,

  Please don't implement your own custom "arena" or "memory pool"
  or "free list" - they will not be accepted."
Donald Knuth uses integers instead of proper pointers in the source code for TeX for maximum portability and performance so your technique is legit used by master programmers but in general replacing pointers with integer indices into arrays only works for monolithic programs of small to medium size. For example, could the Chromium maintainers rewrite the 20 million lines of C++ into Golang replacing most pointers with integer offsets into arrays for performance? No, impossible with current tools and practices, the technique won't scale to that, so this benchmark rule isn't totally stupid and unfair. This binary trees benchmark was originally devised decades ago by Hans Boehm, a notable GC researcher, as a way of testing GC performance that he as a GC implementer found informative.

[1] https://benchmarksgame-team.pages.debian.net/benchmarksgame/...

dandotway··on Go does not need a Java-style GC
Would you mind posting a complete example that compiles and runs? Your above changes to Go#8 break it. E.g. the function 'run' needs to be updated to use your new 'bottomUpTree' and 'inner'.
dandotway··on Go does not need a Java-style GC
Right now in the datacenter CPU usage is considerably more expensive than RAM usage. Ram consumes comparatively little power, whereas burning hot CPUs+GPUs are the reason datacenters are favored near cooling water and power stations. 2.48 vs 12.23 seconds for Java and Go is a big deal for how many solar panels or tons of coal are needed to run an app on Xeon or Epyc instances, whereas 1.7GB vs 0.4GB for Java and Go, a 4x difference in low-power memory usage, is not so big of deal.

At any rate I did link to the full table so everyone can see the mem usage, source listings, etc.

dandotway··on Go does not need a Java-style GC
The binary-trees benchmark on The Debian Language Shootout[1] involves allocating millions of short-lived trees and traversing them. It is informative about GC performance even with the caveat that there are 'lies, damned lies, and benchmarks', because many real-world graph analysis and brute force tree search algorithms similarly allocate zillions of short-lived nodes. For non-GC languages like C/C++/Rust it gives a decent idea of the performance difference between malloc'ing and freeing individual objects vs doing bulk arena allocations:

  language         secs       GC'd language?
  ========         ====       ==============
  C++ (g++)        0.94
  Rust             1.09
  C (gcc)          1.54
  Free Pascal      1.99
  Intel Fortran    2.38
  Java             2.48       yes  <====
  Lisp (SBCL)      2.84       yes
  Ada (GNAT)       3.12
  OCaml            4.68       yes
  Racket           4.81       yes
  C# .NET          4.81       yes
  Haskell (GHC)    5.02       yes
  Erlang           5.19       yes
  F# .NET          6.06       yes
  Node.js          7.20       yes
  Julia            7.43       yes
  Chapel           7.96       yes
  Dart             9.90       yes
  Go              12.23       yes  <====
  Swift           16.15       * "Automatic Reference Counting"
  Smalltalk (VW)  16.33       yes
  PHP             18.64       yes
  Ruby            23.80       yes
  Python 3        48.03       yes
  Lua             48.15       yes
  Perl            53.02       yes
So Java has the fastest GC for this test, 2.48 secs vs 12.23 secs for Golang. The Java code is also notably perfectly idiomatic for multicore, it doesn't do heroic "avoid GC by writing C-like code manipulating a fixed global memory array" tricks. The Java code is also more concise.

The 'plain C' code that uses Apache Portable Runtime memory pools instead of standard malloc/free and uses OpenMP #pragma's strikes me as more 'heroic' than 'idiomatic', whereas C++ and Rust use standard libraries/crates and idiomatic patterns. (Note that OpenMP is 'standard' for high-performance C and well supported across GCC/LLVM/Microsoft/Intel compilers. But still....)

OCaml and Haskell made impressive showings for functional languages which are in practice the easiest for dealing with complicated tree algorithms, which is perhaps why the formally verified C compiler, CompCert, is implemented in OCaml, as is Frama-C for formally verifying ISO C programs, as is the Coq theorem prover, etc.

[1] https://benchmarksgame-team.pages.debian.net/benchmarksgame/... [Edited link]

dandotway··on After 20 Years of Failure, Kill the TSA
Next step: write your local congressional representative with your well-written summary of Directed Attention Fatigue. Unfortunately, your local congressional representative also perhaps suffers Directed Attention Fatigue.
dandotway··on An argument for the impossibility of machine intelligence [pdf]
This was the thesis of Thales of Miletus approximately 2600 years ago, but for the sake of this discussion let's credit Wolfram with the idea since he seems to love credit. ;-)

The human experience of computer programming shows a problem with Wolfram's thought. Wolframism in a nutshell says,

  1. The complicated processes of the universe reduce
     to simple rules (a la Conway's Life).

  2. Therefore, simple rules *produce* the more complicated processes.
     (Or the complicated *emerges* from the simple.)
Consider now that the complexity of computer software "reduces" to simple rules for manipulating 0's and 1's executed on processors, rules like

  - MOVE the sequence of 32 bits from memory address A1 to register R1

  - ADD the sequence of 32 bits in register R1 to register R2 ...
However, these simple rules don't make complicated software---otherwise, many of us here on HN would have to find other work.

Rather, complicated humans make complicated software using these simple rules. (Digression: It's of course too hard to make modern software using these simple rules, so we use complicated toolchains instead to deal with the simple rules.)

Even with Conway's Game of Life, it is often overlooked that in order to actually run a game simulation, you either need to build a very complicated electronic computer to host the "simple" simulation, or you need a complex intelligent life form with a pencil and a great deal of both paper and patience to carry out the rules step-by-step.

Moreover, the simple rules for Conway's Game of Life were created (or discovered?) in the complicated brain of mathematician John Conway. It seems only the most intelligent and complex minds come up with these "simple" mathematical rules like Einstein's "E=mc^2" or Newton's "f=ma".

Also, I know from experience that randomly seeding Conway's Life almost never produces interesting results, such as long lived stable colonies with "gliders" frolicking to and fro. An intelligent human needs to fine tune the initial conditions for the game to get interesting universes that don't quickly become lifeless or stagnant. Interesting universes are sufficiently rare that, when found, are worthy of publishing and nerding out with your friends over.

So Wolframism in its supreme form says the Universe began with simple rules and these simple rules created stars and planets, humans and their brains. But simple rules need a machine to run the rules, a machine more complicated than the rules themselves. And even given a machine to run the rules, most rule sets and most initial configurations produce dead universes.

dandotway··on An argument for the impossibility of machine intelligence [pdf]
The excerpt you quoted is perfectly meaningful. They are saying an evolutionary process that produces intelligent life is more complicated ("has more moving parts") than the intelligent life forms thus produced. How could this not be true? An intelligent life form may have hundreds of billions of neurons and trillions of cells, but the evolution that produced said life form involved untold zillions of complex life forms over billions of years. There are over 10-to-the-power-of-30 microbes on planet earth right now, evolving in ways currently beyond the understanding of any computational biologist.

Although computer scientists can use genetic algorithms inspired by evolution to "breed" better backgammon algorithms, this is quite a few orders of magnitude simpler than emulating a true evolution of intelligent biological life.

The point is intelligent biological life forms are less complicated than the "factory" that produced them.

dandotway··on After 20 Years of Failure, Kill the TSA
My two favorite quotes:

> But the Homeland Security Red Teams in the 2015 test actively concealed forbidden items just as real criminals and terrorist would. The result was that "TSA agents failed 67 out of 70 tests, with Red Team members repeatedly able to get potential weapons through checkpoints."

> What the TSA is good at is high-visibility groping, scanning, and confiscating. Making people drop their pants, take off their shoes, and surrender their shampoo annoys people in a way that says "we're doing something" without actually accomplishing anything. It's what Schneier calls "security theater."

dandotway··on Chess Grandmaster Kasparov on Mob Mentality and Groupthink
archive.ph is one of the archive.today domains. I got the archive.ph link using the archive.today Chrome extension. By "child nudity" do you mean illegal child sex abuse materials? If yes, might want to notify the archive.today maintainers that their archive is being illegally misused. I'm afraid to investigate your claim and try clicking any links in case there really is illegal kiddie content.
← PreviousPage 2 of 6Next →