mpu

18 ms·

31.
by mpu 11y ago
Nope, except for the fun, the assembly part does not add much to the matter. The essence is how to design, describe and analyze algorithms, so it is largely orthogonal to the language you use.
32.
by mpu 11y ago
Pretty good point. That's how I felt. Additionally, this setting is probably too close to usual situations you get in school where there is little to no interaction and negative answers from the teacher are seen as failures by student
33.
by mpu 11y ago
But what a type! I would be much more inclined to annotate effectful code instead.
34.
by mpu 11y ago
I find it hilarious that all the examples he gives in the beginning have weird semantics only because of LAZINESS, mixing effects with laziness gives nonsense, give a cbv semantics to the language and you get the intended behavior (intended
35.
by mpu 11y ago
Agreed.
36.
by mpu 11y ago
Why does it have to be in the cloud? Can't you guys provide a player in html css whatever and the recording program to generate data files for the player so we can use your technology everywhere and are not tied to this website and its
37.
by mpu 11y ago
Good job on the 3-SAT encoding, it was very clear.
38.
by mpu 11y ago
Lots of code in there is deprecated. Don't use it.
39.
by mpu 11y ago
It's not so deep. The takeaway is that modern terrorism will go through wires. Today, the logistics needed to generate massive power failure able to damage severely the economy of all developed countries are arguably simpler than what&
40.
by mpu 11y ago
Maybe it is today, but as soon as it starts to collapse (subprimes and friends), the textbook model has to be saved by external interventions. And so on and so forth. Long term, I doubt pure liberal free markets take us anywhere.
41.
by mpu 11y ago
That's their typical and only way to justify it, indeed. I also feel like they are clueless idiots fighting for small profits and serving a made up ideal of free market. This free market cannot exist because, when left to itself, it co
42.
by mpu 11y ago
The 'extent' you talk about is exactly the lexer (parser) state, you just have to properly serialize it for the beginning of the buffer to get cheap redisplays. It's not rocket science but almost no editor got it right.
43.
by mpu 11y ago
For hardcore users I don't think this tactic suggestion thing is a good idea, for example, how does it deal with custom ltac tactics (cf Chlipala's bedrock)? To prove me wrong one could test the idea on, say, compcert's devel
44.
by mpu 11y ago
The C standard works at an abstraction level that makes it unsuitable for security applications, I would advocate for a new language here. It needs serious PL research with informarion flow reasoning, what we need is just a new kind of lang
45.
by mpu 11y ago
Lto does not work on assembly, it only works if some IR is stored in the .o files (like gimple for gcc) iirc.
46.
by mpu 11y ago
I know the project quite well, it's led by Appel and is called Verified Software Toolchain. They not only compile their code with compcert but also use its correctness theorem to derive the validity of the Assembly code!
47.
by mpu 11y ago
It's not really a 'bit beyond'. The proof is about the machine code that runs on the CPU! It's a huge abstraction gap from C and it is the result of years of formal proofs and PL research. About the effort being worth it
48.
by mpu 11y ago
Writing the definition of sha 256 in Coq must have been of great fun, hehe.
49.
by mpu 11y ago
I'm not a native speaker, I'm sorry you had trouble going through it. I tried to keep it short but maybe did not articulate the first paragraph and the end of the second ideally. Hopefully, you understood the core idea.
50.
Russell's paradox and the Y combinator(c9x.me)
51 points by mpu 11y ago|22 comments
51.
by mpu 11y ago
There is no magic in what the linker is doing. It just needs to create an ELF file with two sections and set the start address. Check this out http://www.muppetlabs.com/~breadbox/software/tiny/teensy.htm...
52.
by mpu 11y ago
Syntax, in assembly, is the least of your problems.
53.
by mpu 11y ago
Is this guy actually writing C++ programs in the wild? He often presents himself as an apostle in the C++ church, but, I am always surprised that he does not seem to apply his guidelines into any practical project of his. As a programmer,
54.
by mpu 11y ago
That's a great project. I was always curious about what makes SSA so special for compiler construction. Can we have more context? Why this book? For who?
55.
by mpu 12y ago
I used it for a while and liked it a lot because it taught me plenty of Haskell. But looking back, I find it a little over-engineered, and the Haskell code seems to be a game of abstraction more than anything else. I don't know what
56.
by mpu 12y ago
Hi, I really like that you use Whitney's style in your javascript! This is a good tribute to this great programmer.
57.
by mpu 12y ago
Written in Go for nothing, you might as well hack a cheap shell script.
58.
by mpu 12y ago
I think it is a nice idea, but I do not agree about the way to implement it. I would like to see more C extensions that work not only following C++'s ideas (dirty syntactic tricks) but are implemented using a proper C parser (like Cil)
59.
by mpu 12y ago
Is this a step towards you understanding you are useless?
60.
by mpu 12y ago
It's unclear what the grand scheme is here. Why using Coq instead of OCaml? How are the theorem proving of Coq used and to prove what? What do we expect from a web server anyway? It is probably an interesting project but I don't s

More ›