Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Come Break My Compiler

bellmar.medium.com

Post reply on HN
Print view View original

11–20 of 33 posts

Re: Come Break My Compiler

#11

Post by avgcorrection »

ggambetta wrote: post #4

> No “real programmers” write code in Assembly. This means the opposite of what she means, which is > No, “real programmers” write code in Assembly. because of the missing comma. Insisting on good spelling and grammar is not about being annoying, it's about not accidentally writing the opposite of what you want to convey :(

EDIT: The following is not not incorrect.

They mean the same thing.

> No “real programmers” write code in Assembly.

Scare quotes for sarcasm/inflection.

Would be better and more idiomatic as a singular noun.

> No, “real programmers” write code in Assembly.

The pause here just marks an interjection/response to something else. But it means the same thing (scare quotes and all).

Re: Come Break My Compiler

#12

Post by Joker_vD »

ggambetta wrote: post #4

> No “real programmers” write code in Assembly. This means the opposite of what she means, which is > No, “real programmers” write code in Assembly. because of the missing comma. Insisting on good spelling and grammar is not about being annoying, it's about not accidentally writing the opposite of what you want to convey :(

I was more perplexed by the usage of the word "dilemma" in the previous sentence, to be fair.

Re: Come Break My Compiler

#13

Post by proto_lambda »

avgcorrection wrote: post #11
ggambetta wrote: post #4

> No “real programmers” write code in Assembly. This means the opposite of what she means, which is > No, “real programmers” write code in Assembly. because of the missing comma. Insisting on good spelling and grammar is not about being annoying, it's about not accidentally writing the opposite of what you want to convey :(

EDIT: The following is not not incorrect. They mean the same thing. > No “real programmers” write code in Assembly. Scare quotes for sarcasm/inflection. Would be better and more idiomatic as a singular noun. > No, “real programmers” write code in Assembly. The pause here just marks an interjection/response to something else. But it means the same thing (scare quotes and all).

> They mean the same thing.

What? No, they don't. The first one means "There are no real programmers who write code in assembly", in other words "Real programmers don't write code in assembly", while the second one means "Real programmers write code in assembly". It is very literally the exact opposite.

Re: Come Break My Compiler

#14

Post by lou1306 »

laserbeam wrote: post #2

My only knowledge on modeling languages is: TLA+ exists, I've seen Lamport's introductory videos/course, I've followed along to the course examples. At a glance, I like that this looks more approachable to write, and I like that. Can it still be used to prove properties like liveliness? The fact that Fault seems to use bounded loops seems counter-intuitive to proving those "x eventually happens" conditions. As I unde…

(Just for the sake of nitpicking: the term is "liveness")

Short answer is no (seemingly). From the docs it seems Fault only supports assertions. Finding an assertion violation is a reachability problem and is immediately usable to prove safety problems, not liveness.

But, long answer is "kind of"!

That a counterexample to a liveness property ("x eventually happens") generally is a lasso-shaped execution (so a prefix + a cycle) where x never happens. With that in mind, you can reduce liveness checking to reachability: the only problem is, you have to add state-tracking to your model and assert "the system never closes a cycle when x never happens".

This is explained in detail, e.g., in Armin Biere, Cyrille Artho, and Viktor Schuppan. 2002. Liveness Checking as Safety Checking. Electron. Notes Theor. Comput. Sci. 66, 2 (2002), 160–177. DOI:https://doi.org/10.1016/S1571-0661(04)80410-9

Re: Come Break My Compiler

#15

Post by avgcorrection »

proto_lambda wrote: post #13
avgcorrection wrote: post #11

Earlier quoted context omitted.

EDIT: The following is not not incorrect. They mean the same thing. > No “real programmers” write code in Assembly. Scare quotes for sarcasm/inflection. Would be better and more idiomatic as a singular noun. > No, “real programmers” write code in Assembly. The pause here just marks an interjection/response to something else. But it means the same thing (scare quotes and all).

> They mean the same thing. What? No, they don't. The first one means "There are no real programmers who write code in assembly", in other words "Real programmers don't write code in assembly", while the second one means "Real programmers write code in assembly". It is very literally the exact opposite.

Dang. You’re right.

Re: Come Break My Compiler

#16

Post by laserbeam »

lou1306 wrote: post #14
laserbeam wrote: post #2

My only knowledge on modeling languages is: TLA+ exists, I've seen Lamport's introductory videos/course, I've followed along to the course examples. At a glance, I like that this looks more approachable to write, and I like that. Can it still be used to prove properties like liveliness? The fact that Fault seems to use bounded loops seems counter-intuitive to proving those "x eventually happens" conditions. As I unde…

(Just for the sake of nitpicking: the term is "liveness") Short answer is no (seemingly). From the docs it seems Fault only supports assertions. Finding an assertion violation is a reachability problem and is immediately usable to prove safety problems, not liveness. But, long answer is "kind of"! That a counterexample to a liveness property ("x eventually happens") generally is a lasso-shaped execution (so a prefix…

> (Just for the sake of nitpicking: the term is "liveness")

I appreciate the nitpick, I'm new to this :).

Re: Come Break My Compiler

#17

Post by cinntaile »

avgcorrection wrote: post #10
benj111 wrote: post #5

Earlier quoted context omitted.

While I'd never heard of the language or compiler before, so unless you want a title that covers the blog post, I don't know how you want to get rid of your objections.

Blog post with submission title: “Fault is a language for modeling systems that compiles down to SMT” This is in the power of the submitter since the submitter is the author of this piece.

That would be an incorrect description of the content. The point of the article isn't to introduce the language, the point is to sollicit feedback.

Re: Come Break My Compiler

#18

Post by aprilnya »

avgcorrection wrote: post #3

Useless title for HN.[1] A compiler tells me that it’s some language that can be compiled. “Break” tells me that either the compiler is mature and the author is daring someone to fuzz it, or that the compiler is not mature and hence it’s easy to find something that “breaks” while using it (it’s the latter). Would I break someone’s program? I have no reason to care about their program based on this title. [1] Of cours…

The title isn’t editorialized. The title on HN is exactly the same as the original blog post

Re: Come Break My Compiler

#19

Post by oneeyedpigeon »

ggambetta wrote: post #4

> No “real programmers” write code in Assembly. This means the opposite of what she means, which is > No, “real programmers” write code in Assembly. because of the missing comma. Insisting on good spelling and grammar is not about being annoying, it's about not accidentally writing the opposite of what you want to convey :(

The real flaw is that we've overloaded "no" to mean "zero" as well as the opposite of "yes". Without that ambiguity, the sentence would be fine (even if a comma were still technically correct).

Re: Come Break My Compiler

#20

Post by lo_zamoyski »

ggambetta wrote: post #4

> No “real programmers” write code in Assembly. This means the opposite of what she means, which is > No, “real programmers” write code in Assembly. because of the missing comma. Insisting on good spelling and grammar is not about being annoying, it's about not accidentally writing the opposite of what you want to convey :(

> Insisting on good spelling and grammar is not about being annoying, it's about not accidentally writing the opposite of what you want to convey :(

True, but in this case, you were able to infer the intended meaning from context, which is what reading is: interpreting text, which involves assigning meanings to symbols and resolving ambiguities to render the whole as intelligible as possible. Since nothing can be drawn out of the text per se, this means you are the one bringing all the meaning to the text. Whatever the author is conveying is, in one way or another, latent in the context that's already in your mind. Even fiction is composed of elements already in your mind.

(Which is why a lack of experience can be an obstacle to effective reading.)

Post reply on HN