mpu

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's necessary to re-create a 9-11.

I think we should fear and get ready, unit testing and agile software are not enough. We need to make sure some systems are NOT reachable in any way via internet, we need formal methods and expensive secure designs.

I really hope terrorists never get smart enough to attack digital infrastructures.

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.

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 collapses. To remedy that, it's government funded and the money that goes into those Wall Street's geniuses is simply taxpayers'.

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.

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 development and compute how often the next tactic is among the suggested ones.

On the other hand, One common problem in large proofs is having too many hypothesis in stock, one super nice extension would be to quantify the relevance of each and color/display them accordingly, leaving the option to move the 'tolerance' threshold for display. This relevance metric would have to be aware if lemmas available (of A -> B is proved by a lemma, and B is the goal, A is relevant).

My 2 cts.

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 language much more machine aware (yes, more low-level) than C.

Lto does not work on assembly, it only works if some IR is stored in the .o files (like gimple for gcc) iirc.

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!

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 or not, I believe that security critical programs MUST have formal proofs. Vulnerabilities in this kind of software are extremely costly. The same goes for software whose failure can be of danger for humans (c.f. the Toyota debacle).

Writing the definition of sha 256 in Coq must have been of great fun, hehe.

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.

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...

Syntax, in assembly, is the least of your problems.

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, I'm suspicious when people have opinions and give advice but never showed me more than snippets of code. Like a master tailor that wouldn't sew. How come he gets that much recognition and respect?

I would be much more inclined into accepting advice from someone like, say, Carmack, that has successful projects in C++ under his belt. (Many people consider Doom 3's code beautiful C++, yet, the choices made there are very controversial, and far from "modern".)

I also put Bjarne Stroustrup in the same category.

What do you think?

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?

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 point they are proving, but a lot of code seems to be over-parameterized. IMO, these superfluous generalizations make the code opaque to beginners while not adding much functionality. This coding style seems to be a general trait (if I may) of the Haskell programs that is not present in typical OCaml code (which is why I tend to prefer the latter).

Hi, I really like that you use Whitney's style in your javascript! This is a good tribute to this great programmer.

Written in Go for nothing, you might as well hack a cheap shell script.

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) and principled program transformations (i.e. compilation).

Maybe we need a classier framework than Gnu C and macros to toy around with C extensions...

Is this a step towards you understanding you are useless?

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 see anything else on their website that witnesses more than the fact that they can write monadic code.

You are right. But these problems can be solved using annotations.

Your comment helped me to narrow my complaint: While functional languages require annotations for things that are not obvious (when to subclass, when to change the type of an object, what overload should I use) and infer the obvious ("n*fact(n-1)" is an integer); C++ infers the non-obvious and requires you to add annotations on the obvious!

Phrased that way, it is striking.

> Can you master all compiler specific behaviours not covered by the standard?!?

No, and the good part is: I don't need to :). All my programs are standard C11 (- concurrency).

I am not sure what C++ brings in as a language.

If you want to get an idea how your code will work or even if it going to work at all you have to first understand type deduction rules which are seemingly completely unprincipled. When I compare the "rules" of C++ type deduction to functional languages' type inference algorithms I can easily understand how the latter work but I have no clue about what justifies the former.

Yet, in C++, if I want auto type inference on my recursive factorial function I have to write "return 1;" syntactically before (i.e. where the order is the relative position of bytes fed to the compiler) "return n*fact(n-1);", otherwise the compiler is unable to find the type. I just don't understand. The type deduction rules (say reference collapsing) are rocket science and take a full blog post as their justification, but basic unification algorithms known in the PL community for literally decades cannot be implemented in the standard?

This language seems plain crazy, this kind of article makes me wonder why people think it can be a reasonable choice for any kind of software project.

At least, C can fit in a brain.

They are not modules.

Here is a short list of things that you can't do with these C structs. Modules can be "opened", they can store types, and they can be compiled efficiently (calling a function in a struct will always cost an indirection). Also, a proper implementation of modules would allow to obsolete the pre-processor and header files, this is not solved by your proposal.

In short, your solution is no different than prefixing each function name with the "module" name, M_foo, M_bar,...

You can look at (this)[http://llvm.org/devmtg/2012-11/Gregor-Modules.pdf] for a better proposal.

I'm glad to see such a positive reaction! I worked on that for quite a while and use it daily. I think the code is of pretty good quality (never had a segfault or data loss while using it). If you try it and encounter annoyances because it does not behave exactly like what you want, you have to hack in the code! I will never fix something myself if it does not annoy me. This does not mean that I did nothing for you, instead I tried a lot to make the code such that everybody can hack it, it is very regular, short, simple and occasionally well documented (vicmd.w, buf.c).

I spent a probably unreasonable amount of time thinking on its design and I believe I came up with something satisfying, the code is only 3000 lines but one or two features I want remain to be hacked in. The undo and the buffer data structures were tested automatically for several hours with success (see the tools/ subdir), no data was ever lost. The file saving command is even formally proved correct in Coq.

Any suggestion that could simplify the logic and preferably decrease the line count is more than welcome.

Also, note that the version showed in the video is a bit deprecated, the master branch now supports better handling of async commands and window splits (vertical and up to 6 windows) with resizes using the mouse.

Some are concerned about the license. It is public domain. But please tell me if you do something cool with it or like it.

The reasons you cite are the reasons why it is that way. Concerning the 'c' command, I leave it that way until people are so annoyed that they have to dive in the code themselves, it is a kind of social experiment. I got used to not using it.

I went through lots of thinking to make the code nice and clean and would like to see if it is indeed that way by having people modify it.

I thought it could be fun to include it in the documentation. Why not, after all. This is a good read. It turns out that I also used it for tests, if the editor behaves smoothly on this file I judge it fast enough.

Splits are available in the git master branch.

I hacked it. It's public domain for now. I might (or not) switch to MIT later.