1 files changed, 102 insertions, 0 deletions
diff --git a/content/zettel/1d1.md b/content/zettel/1d1.md
new file mode 100644
index 0000000..dcd131c
--- /dev/null
+++ b/content/zettel/1d1.md
@@ -0,0 +1,102 @@
++++
+title = "Bluespec"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["1d"]
+forwardlinks = ["1b2", "3a", "1b1"]
+zettelid = "1d1"
++++
+
+Bluespec is a higher-level hardware description language, based on
+circuit generation instead of circuit description.
+
+{{< transclude-1 zettel="1b2" >}}
+
+Tail calls are an optimisation that can be applied in software, which
+detects that a recursive call only happens at the tail of the function.
+If that is the case, then the recursive call can happen without having
+to preserve the stack at every call, as it can effectively be translated
+to an equivalent version that only uses loops. This optimisation is
+important to improve the efficiency of recursive functions if the stack
+is not needed, and is especially important in functional languages where
+recursion might be more widely used.
+
+As tail calls can be efficiently translated to loops, this also means
+that they can be efficiently encoded in hardware when the code is passed
+through high-level synthesis. This is straightforward if the tail calls
+are detected and automatically translated to loops, however, what
+happens if that is not the case and we only have a tail call construct
+in the intermediate language.
+
+The CompCert ([\#3a]) \[1\] register transfer language (RTL)
+intermediate language, for example, has an explicit tail call construct
+(`Itailcall`), which is used if it can detect that a function contains a
+tail call. Apart from that, it only has a jump command, which can be
+used for loops. Therefore, supporting the tail call construct allows us
+to support a subset of possible recursive functions. Even though these
+are as powerful as loops, it may be more natural to write their
+definitions as a recursive function instead of a loop.
+
+{{< transclude-2 zettel="1b1" >}}
+
+Guarded commands \[2\] are an interesting construct which can be added
+to languages. They look similar to `case` statements, but behave in a
+parallel and nondeterministic way. Each guard has a boolean value
+followed by a program which may be executed if the guard evaluates to
+true. The following shows the main syntax that guards may have.
+
+``` grammar
+e ::= if gc fi | do gc od ...
+
+gc ::= (b e) || gc
+```
+
+One reason these are interesting language constructs, is because they
+allow for the encoding of commands that may be executed when a condition
+is true, but that it isn't necessary. Often, when giving instructions,
+one does not really specify the order, just the commands that should
+eventually be executed.
+
+The guarded commands `gc` will either return a match if a boolean
+evaluates to true, or `abort`. There are two constructs that are built
+around guarded commands which adds more functionality to them.
+`if gc fi` matches one rule in the guarded statement and executes it. If
+it does not match a rule, it then acts like `abort`. `do gc od` loops
+over the guarded commands while any rule matches. If there no match is
+found, it acts like `skip`.
+
+These allow for nice encoding of common algorithms, using two other
+constructs that use the guarded commands.
+
+{{< /transclude-2 >}}
+
+{{< /transclude-1 >}}
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">X. Leroy, “Formal certification of
+a compiler back-end or: Programming a compiler with a proof assistant,”
+in *Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on
+principles of programming languages*, in POPL ’06. Charleston, South
+Carolina, USA: Association for Computing Machinery, 2006, pp. 42–54.
+doi: [10.1145/1111037.1111042].</span>
+
+</div>
+
+<div id="ref-winskel93" class="csl-entry" markdown="1">
+
+<span class="csl-left-margin">\[2\]
+</span><span class="csl-right-inline">G. Winskel, *The formal semantics
+of programming languages: An introduction*. MIT press, 1993.</span>
+
+</div>
+
+</div>
+
+  [\#3a]: /zettel/3a
+  [10.1145/1111037.1111042]: https://doi.org/10.1145/1111037.1111042