5 ms·

Come Break My Compiler

116 points by mbellotti 4y ago

laserbeam 4y ago
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 understand (from a distance) you can model those in TLA+. PS. The question regards the design of Fault, not the current state of implementation.
- lou1306 4y ago
  (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 https://doi.org/10.1016/S1571-0661(04)80410-9
  - laserbeam 4y ago
    > (Just for the sake of nitpicking: the term is "liveness") I appreciate the nitpick, I'm new to this :).
avgcorrection 4y ago
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 course there’s the “no ediotoralizing” rule. Even though it’s submitted by the original author.
- benj111 4y ago
  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.
  - avgcorrection 4y ago
    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.
    - cinntaile 4y ago
      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.
- cinntaile 4y ago
  The article perfectly explains why the author wants you to break the compiler. It's so it can be improved and to do that user feedback (by breaking the compiler) is needed.
  - avgcorrection 4y ago
    “Test my software” I’ll get right on that.
- aprilnya 4y ago
  The title isn’t editorialized. The title on HN is exactly the same as the original blog post
  - avgcorrection 4y ago
    Of course it isn’t. That’s what I wrote. “Of course there’s the “no ediotoralizing” rule” to acknowledge and preempt the “no editorializing” responses. But (as I wrote) the submitter and the author are the same person.
ggambetta 4y ago
> 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 :(
- junon 4y ago
  Amazingly, I knew exactly what she meant. It's also entirely aside from the point of the article, and either interpretation still works toward making her underlying point.
  - shiomiru 4y ago
    I understood the intention behind the sentence as well, after all it's a common joke. However, it also distracted me from the post, and lead me to think about spelling instead of the author's compiler... which I don't think was intended.
    - junon 4y ago
      I respectfully disagree this is a problem for the author to fix.
- avgcorrection 4y ago
  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).
  - proto_lambda 4y ago
    > 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.
ChicagoDave 4y ago
This seems procedural to me and modern architectures lean towards events, boundaries, and language. I get it, but it’s not how I decipher and construct models.
remon 4y ago
I quite like this approach to system spec languages. It feels a bit more modern than the rather unwieldy TLA+. Can someone explain how a spec language can exist without sets as a first class datatype though? (admittedly I only had time for a cursory glance at Fault). Also had a quick look at the codebase and was positively surpised by it being Golang. Oh and just in case the author has a peek at this thread; the only source file I opened had this interesting typo :D "NewProcesser() *Processor"
camgunz 4y ago
Nice that this is now real! I followed along with Marianne Writes a Programming Language [0] which I thoroughly enjoyed, and it's cool to see this come to fruition. [0]: https://bellmar.medium.com/marianne-writes-a-programming-language-8fff3e09f3e https://bellmar.medium.com/marianne-writes-a-programming-lan...

116 points by mbellotti 4y ago

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 understand (from a distance) you can model those in TLA+. PS. The question regards the design of Fault, not the current state of implementation.

lou1306 4y ago
(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 https://doi.org/10.1016/S1571-0661(04)80410-9
- laserbeam 4y ago
  > (Just for the sake of nitpicking: the term is "liveness") I appreciate the nitpick, I'm new to this :).

avgcorrection 4y ago

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 course there’s the “no ediotoralizing” rule. Even though it’s submitted by the original author.

benj111 4y ago
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.
- avgcorrection 4y ago
  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.
  - cinntaile 4y ago
    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.
cinntaile 4y ago
The article perfectly explains why the author wants you to break the compiler. It's so it can be improved and to do that user feedback (by breaking the compiler) is needed.
- avgcorrection 4y ago
  “Test my software” I’ll get right on that.
aprilnya 4y ago
The title isn’t editorialized. The title on HN is exactly the same as the original blog post
- avgcorrection 4y ago
  Of course it isn’t. That’s what I wrote. “Of course there’s the “no ediotoralizing” rule” to acknowledge and preempt the “no editorializing” responses. But (as I wrote) the submitter and the author are the same person.

ggambetta 4y ago

> 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 :(

junon 4y ago
Amazingly, I knew exactly what she meant. It's also entirely aside from the point of the article, and either interpretation still works toward making her underlying point.
- shiomiru 4y ago
  I understood the intention behind the sentence as well, after all it's a common joke. However, it also distracted me from the post, and lead me to think about spelling instead of the author's compiler... which I don't think was intended.
  - junon 4y ago
    I respectfully disagree this is a problem for the author to fix.
avgcorrection 4y ago
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).
- proto_lambda 4y ago
  > 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.

ChicagoDave 4y ago

This seems procedural to me and modern architectures lean towards events, boundaries, and language. I get it, but it’s not how I decipher and construct models.

remon 4y ago

I quite like this approach to system spec languages. It feels a bit more modern than the rather unwieldy TLA+. Can someone explain how a spec language can exist without sets as a first class datatype though? (admittedly I only had time for a cursory glance at Fault). Also had a quick look at the codebase and was positively surpised by it being Golang. Oh and just in case the author has a peek at this thread; the only source file I opened had this interesting typo :D "NewProcesser() *Processor"

camgunz 4y ago

Nice that this is now real! I followed along with Marianne Writes a Programming Language [0] which I thoroughly enjoyed, and it's cool to see this come to fruition. [0]: https://bellmar.medium.com/marianne-writes-a-programming-language-8fff3e09f3e https://bellmar.medium.com/marianne-writes-a-programming-lan...