dandotway

10 ms·

31.
by dandotway 5y ago
I just went through the CBMC tutorial[1] to make sure I'm not crazy. Yes, CBMC is a bounded model checker, as I thought. CBMC can also be used for programs with unbounded loops. In this case, CBMC is used for bug hunting only; CB
32.
by dandotway 5y ago
"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 boi
33.
by dandotway 5y ago
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
34.
by dandotway 5y ago
> 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-const
35.
by dandotway 5y ago
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
36.
by dandotway 5y ago
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
37.
by dandotway 5y ago
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
38.
by dandotway 5y ago
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
39.
by dandotway 5y ago
Many word have trick. Make see different than few word.
40.
by dandotway 5y ago
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 anc
41.
by dandotway 5y ago
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,
42.
by dandotway 5y ago
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 equival
43.
by dandotway 5y ago
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 ho
44.
by dandotway 5y ago
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 doe
45.
by dandotway 5y ago
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
46.
Historically Black College grads average $927,000 more throughout career(wsj.com)
5 points by dandotway 5y ago|1 comments
47.
by dandotway 5y ago
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 singl
48.
by dandotway 5y ago
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/T
49.
by dandotway 5y ago
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 conso
50.
by dandotway 5y ago
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.debia
51.
by dandotway 5y ago
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 see
52.
by dandotway 5y ago
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_mu
53.
by dandotway 5y ago
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
54.
by dandotway 5y ago
+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 pointe
55.
by dandotway 5y ago
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'.
56.
by dandotway 5y ago
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 v
57.
by dandotway 5y ago
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 ben
58.
by dandotway 5y ago
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.
59.
by dandotway 5y ago
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 probl
60.
by dandotway 5y ago
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

More ›