rebuild

utahplt · Jul 31, 2024 · 36fc95c · 36fc95c
1 parent 4966e5d
commit 36fc95c
Show file tree

Hide file tree

Showing 6 changed files with 43 additions and 36 deletions.
diff --git a/.frog/build b/.frog/build
@@ -1 +1 @@
-((3) 0 () 9 ((p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) (u . "") (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2023-09-19-generating-programs-trivially.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-04-21-forge.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-02-02-luau-telemetry.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-07-26-type-tailoring.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-07-07-ltlf.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix)) () (h ! (equal) ((? . 0) f post (u . "[Conceptual Mutation Testing](https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html)") (? . 0) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html" . unix) (u . "/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html") (u . "2023-10-31T01:11:11") (? . 2) (? . 4) () (? . 1) #f (? . 1)) ((? . 2) f post (u . "[Generating Programs Trivially: Student Use of Large Language Models](https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html)") (? . 2) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html" . unix) (u . "/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html") (u . "2023-09-19T01:11:11") (? . 7) (? . 0) () (? . 1) #f (? . 1)) ((? . 3) f post (u . "[Forge: A Tool to Teach Formal Methods](https://blog.brownplt.org/2024/04/21/forge.html)") (? . 3) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html" . unix) (u . "/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html") (u . "2024-04-21T01:11:11") (? . 4) (? . 6) () (? . 1) #f (? . 1)) ((? . 4) f post (u . "[Privacy-Respecting Type Error Telemetry at Scale](https://blog.brownplt.org/2024/02/02/privacy-telemetry.html)") (? . 4) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html" . unix) (u . "/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html") (u . "2024-02-02T01:11:11") (? . 0) (? . 3) () (? . 1) #f (? . 1)) ((? . 5) f post (u . "[Evolving Languages Faster with Type Tailoring](https://lambdaland.org/posts/2024-07-15_type_tailoring/)") (? . 5) 1722024520 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html" . unix) (u . "/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html") (u . "2024-07-26T14:07:34") (? . 6) #f () (? . 1) #f (? . 1)) ((? . 6) f post (u . "[Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic](https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html)") (? . 6) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html" . unix) (u . "/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html") (u . "2024-07-07T01:11:11") (? . 3) (? . 5) () (? . 1) #f (? . 1)) ((? . 7) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 7) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/06/gtp-benchmarks-for-gradual-typing-performance.html" . unix) (u . "/2023/06/gtp-benchmarks-for-gradual-typing-performance.html") (u . "2023-06-28T17:18:44") (? . 8) (? . 2) (c (u . "by Ben Greenman")) (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>") #t (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>\n<!-- more-->\n\n<hr />\n\n<p>What on earth is gradual typing performance and why does it matter?</p>\n\n<p>The second question is easy to answer: performance matters because the cost of gradual types can slow a program by several <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#tfgnvf-popl-2016\">orders of magnitude</a>. To answer the first question, we need to step back a bit&hellip;</p>\n\n<p>Normally, a type system is an ahead-of-time thing. Programs must typecheck before they can run. Afterwards, types can disappear. Compiled code can safely run full-throttle and assume that everything in its world behaves in a well-typed way.</p>\n\n<p>Gradual typing leads to an entirely different situation. It allows typed and untyped code to live together, which means that part of the codebase might rely on type assumptions that the rest of the codebase does not know about!</p>\n\n<p>Suppose we have a typed function that averages the elements in a list:</p>\n\n<div class=\"brush: python\">\n <pre><code>def avg(nums: list[int]):\n  ....</code></pre></div>\n\n<p>This function expects inputs that have the type <code>list[int]</code>. The typechecker will make sure that every call to <code>avg</code> in typed code match this expectation. But the typechecker will not check any calls to <code>avg</code> that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!</p>\n\n<p>Consequently, untyped code can ask outrageous questions when the program runs:</p>\n\n<pre><code>avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)</code></pre>\n\n<p>We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?</p>\n\n<ul>\n <li>One option is to do nothing. Let the programmer beware that gradual  types are unsound at the boundaries to untyped code.  With this mindset, types remain cost-free but give zero help for debugging.  Many languages follow this approach, including TypeScript and mypy.</li>\n <li>Another option is to enforce type soundness with runtime checks.  Now we have reliable types (to some extent), but we also have costs  to measure and minimize.</li></ul>\n\n<p>The GTP Benchmarks are a collection of 21 programs designed to test the costs of sound gradual types. Each program comes in two forms, untyped and typed (written in Racket and Typed Racket), with the crucial property that any module-by-module mix of the two forms results in a working program. A benchmark with <code>N</code> modules generates <code>2^N</code> partially-typed programs that sample the space of gradual possibilities:</p>\n\n<p><img src=\"/img/gtp-lattice.png\" width=\"50%\" /></p>\n\n<p>The table below is a birds-eye view of the benchmarks. It lists their name, purpose, and characteristics: whether they were originally typed (T Init), whether they depend on untyped (U Lib) or typed (T Lib) library code, whether they define generative datatypes (Adapt), and whether they send higher-order function (HOF), polymorphic types (Poly), recursive types (Rec), mutable data-structure types (Mut), immutable data-structure types (Imm), object types (Obj), or class types (Cls) across any untyped boundary:</p>\n\n<p><img src=\"/img/gtp-programs.png\" /></p>\n\n<p>For more details, see <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#g-rep-2023\">the paper</a>.</p>")) ((? . 8) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 8) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2023-06-26T01:11:11") #f (? . 7) () (? . 1) #f (? . 1))))
+((3) 0 () 9 ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-26-type-tailoring.md" . unix) (u . "") (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-04-21-forge.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-07-ltlf.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-02-02-luau-telemetry.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-09-19-generating-programs-trivially.md" . unix)) () (h ! (equal) ((? . 0) f post (u . "[Evolving Languages Faster with Type Tailoring](https://lambdaland.org/posts/2024-07-15_type_tailoring/)") (? . 0) 1722436704 (p+ #"/Users/ben/code/uu/blog/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html" . unix) (u . "/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html") (u . "2024-07-26T14:07:34") (? . 3) #f () (? . 1) #f (? . 1)) ((? . 2) f post (u . "[Forge: A Tool to Teach Formal Methods](https://blog.brownplt.org/2024/04/21/forge.html)") (? . 2) 1719613724 (p+ #"/Users/ben/code/uu/blog/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html" . unix) (u . "/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html") (u . "2024-04-21T01:11:11") (? . 5) (? . 3) () (? . 1) #f (? . 1)) ((? . 4) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 4) 1720879367 (p+ #"/Users/ben/code/uu/blog/2023/06/gtp-benchmarks-for-gradual-typing-performance.html" . unix) (u . "/2023/06/gtp-benchmarks-for-gradual-typing-performance.html") (u . "2023-06-28T17:18:44") (? . 6) (? . 8) (c (u . "by Ben Greenman")) (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>") #t (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>\n<!-- more-->\n\n<hr />\n\n<p>What on earth is gradual typing performance and why does it matter?</p>\n\n<p>The second question is easy to answer: performance matters because the cost of gradual types can slow a program by several <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#tfgnvf-popl-2016\">orders of magnitude</a>. To answer the first question, we need to step back a bit&hellip;</p>\n\n<p>Normally, a type system is an ahead-of-time thing. Programs must typecheck before they can run. Afterwards, types can disappear. Compiled code can safely run full-throttle and assume that everything in its world behaves in a well-typed way.</p>\n\n<p>Gradual typing leads to an entirely different situation. It allows typed and untyped code to live together, which means that part of the codebase might rely on type assumptions that the rest of the codebase does not know about!</p>\n\n<p>Suppose we have a typed function that averages the elements in a list:</p>\n\n<div class=\"brush: python\">\n <pre><code>def avg(nums: list[int]):\n  ....</code></pre></div>\n\n<p>This function expects inputs that have the type <code>list[int]</code>. The typechecker will make sure that every call to <code>avg</code> in typed code match this expectation. But the typechecker will not check any calls to <code>avg</code> that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!</p>\n\n<p>Consequently, untyped code can ask outrageous questions when the program runs:</p>\n\n<pre><code>avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)</code></pre>\n\n<p>We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?</p>\n\n<ul>\n <li>One option is to do nothing. Let the programmer beware that gradual  types are unsound at the boundaries to untyped code.  With this mindset, types remain cost-free but give zero help for debugging.  Many languages follow this approach, including TypeScript and mypy.</li>\n <li>Another option is to enforce type soundness with runtime checks.  Now we have reliable types (to some extent), but we also have costs  to measure and minimize.</li></ul>\n\n<p>The GTP Benchmarks are a collection of 21 programs designed to test the costs of sound gradual types. Each program comes in two forms, untyped and typed (written in Racket and Typed Racket), with the crucial property that any module-by-module mix of the two forms results in a working program. A benchmark with <code>N</code> modules generates <code>2^N</code> partially-typed programs that sample the space of gradual possibilities:</p>\n\n<p><img src=\"/img/gtp-lattice.png\" width=\"50%\" /></p>\n\n<p>The table below is a birds-eye view of the benchmarks. It lists their name, purpose, and characteristics: whether they were originally typed (T Init), whether they depend on untyped (U Lib) or typed (T Lib) library code, whether they define generative datatypes (Adapt), and whether they send higher-order function (HOF), polymorphic types (Poly), recursive types (Rec), mutable data-structure types (Mut), immutable data-structure types (Imm), object types (Obj), or class types (Cls) across any untyped boundary:</p>\n\n<p><img src=\"/img/gtp-programs.png\" /></p>\n\n<p>For more details, see <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#g-rep-2023\">the paper</a>.</p>")) ((? . 5) f post (u . "[Privacy-Respecting Type Error Telemetry at Scale](https://blog.brownplt.org/2024/02/02/privacy-telemetry.html)") (? . 5) 1719613751 (p+ #"/Users/ben/code/uu/blog/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html" . unix) (u . "/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html") (u . "2024-02-02T01:11:11") (? . 7) (? . 2) () (? . 1) #f (? . 1)) ((? . 6) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 6) 1720882180 (p+ #"/Users/ben/code/uu/blog/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2023-06-26T01:11:11") #f (? . 4) () (? . 1) #f (? . 1)) ((? . 3) f post (u . "[Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic](https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html)") (? . 3) 1720817329 (p+ #"/Users/ben/code/uu/blog/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html" . unix) (u . "/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html") (u . "2024-07-07T01:11:11") (? . 2) (? . 0) () (? . 1) #f (? . 1)) ((? . 7) f post (u . "[Conceptual Mutation Testing](https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html)") (? . 7) 1719613783 (p+ #"/Users/ben/code/uu/blog/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html" . unix) (u . "/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html") (u . "2023-10-31T01:11:11") (? . 8) (? . 5) () (? . 1) #f (? . 1)) ((? . 8) f post (u . "[Generating Programs Trivially: Student Use of Large Language Models](https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html)") (? . 8) 1719613991 (p+ #"/Users/ben/code/uu/blog/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html" . unix) (u . "/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html") (u . "2023-09-19T01:11:11") (? . 4) (? . 7) () (? . 1) #f (? . 1))))
diff --git a/...ages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html b/...ages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html
@@ -25,10 +25,14 @@
     <div class="container">
       <div class="row">
         <!-- Main column -->
-        <div id="content" class="col-md-12">
+        <div id="content" class="col-md-9">
+          <a href="https://www-old.cs.utah.edu/plt/">
           <H1>
-          <IMG SRC="/img/logo.gif" ALIGN=center ALT="[PLT logo]">&nbsp;Utah PLT Blog
+          <img src="/img/utahplt.svg" style="margin: -10px 0 -60px -40px;" width="40%" alt="[Utah PLT logo]">
           </H1>
+          </a>
+        </div>
+        <div id="content" class="col-md-3">
         </div>
         <div class="col-md-3">
           <a href="/feeds/all.rss.xml">
@@ -55,6 +59,9 @@ <h2><a href="https://lambdaland.org/posts/2024-07-15_type_tailoring/">Evolving L
         <p>Site generated
         by <a href="https://github.com/greghendershott/frog">Frog</a>,
         the <strong>fr</strong>ozen bl<strong>og</strong> tool.</p>
+        <div class="col-md-12">
+          <img src="/img/logo.gif" width="10%" alt="[Utah PLT logo]"/>
+        </div>
       </footer>
     </div>
   </body>

diff --git a/...linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html b/...linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html
@@ -10,7 +10,7 @@
     <link rel="icon"      href="/favicon.ico">
     <link rel="canonical" href="https://www-old.cs.utah.edu/plt//2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html">
     <link rel="next" href="/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html">
-
+    <link rel="prev" href="/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html">
     <!-- CSS -->
     <link rel="stylesheet" type="text/css" href="/css/bootstrap.min.css">
     <link rel="stylesheet" type="text/css" href="/css/pygments.css">
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		((3) 0 () 9 ((p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) (u . "") (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2023-09-19-generating-programs-trivially.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-04-21-forge.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-02-02-luau-telemetry.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-07-26-type-tailoring.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-07-07-ltlf.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix)) () (h ! (equal) ((? . 0) f post (u . "[Conceptual Mutation Testing](https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html)") (? . 0) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html" . unix) (u . "/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html") (u . "2023-10-31T01:11:11") (? . 2) (? . 4) () (? . 1) #f (? . 1)) ((? . 2) f post (u . "[Generating Programs Trivially: Student Use of Large Language Models](https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html)") (? . 2) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html" . unix) (u . "/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html") (u . "2023-09-19T01:11:11") (? . 7) (? . 0) () (? . 1) #f (? . 1)) ((? . 3) f post (u . "[Forge: A Tool to Teach Formal Methods](https://blog.brownplt.org/2024/04/21/forge.html)") (? . 3) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html" . unix) (u . "/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html") (u . "2024-04-21T01:11:11") (? . 4) (? . 6) () (? . 1) #f (? . 1)) ((? . 4) f post (u . "[Privacy-Respecting Type Error Telemetry at Scale](https://blog.brownplt.org/2024/02/02/privacy-telemetry.html)") (? . 4) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html" . unix) (u . "/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html") (u . "2024-02-02T01:11:11") (? . 0) (? . 3) () (? . 1) #f (? . 1)) ((? . 5) f post (u . "[Evolving Languages Faster with Type Tailoring](https://lambdaland.org/posts/2024-07-15_type_tailoring/)") (? . 5) 1722024520 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html" . unix) (u . "/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html") (u . "2024-07-26T14:07:34") (? . 6) #f () (? . 1) #f (? . 1)) ((? . 6) f post (u . "[Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic](https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html)") (? . 6) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html" . unix) (u . "/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html") (u . "2024-07-07T01:11:11") (? . 3) (? . 5) () (? . 1) #f (? . 1)) ((? . 7) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 7) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/06/gtp-benchmarks-for-gradual-typing-performance.html" . unix) (u . "/2023/06/gtp-benchmarks-for-gradual-typing-performance.html") (u . "2023-06-28T17:18:44") (? . 8) (? . 2) (c (u . "by Ben Greenman")) (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>") #t (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>\n<!-- more-->\n\n<hr />\n\n<p>What on earth is gradual typing performance and why does it matter?</p>\n\n<p>The second question is easy to answer: performance matters because the cost of gradual types can slow a program by several <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#tfgnvf-popl-2016\">orders of magnitude</a>. To answer the first question, we need to step back a bit…</p>\n\n<p>Normally, a type system is an ahead-of-time thing. Programs must typecheck before they can run. Afterwards, types can disappear. Compiled code can safely run full-throttle and assume that everything in its world behaves in a well-typed way.</p>\n\n<p>Gradual typing leads to an entirely different situation. It allows typed and untyped code to live together, which means that part of the codebase might rely on type assumptions that the rest of the codebase does not know about!</p>\n\n<p>Suppose we have a typed function that averages the elements in a list:</p>\n\n<div class=\"brush: python\">\n <pre><code>def avg(nums: list[int]):\n ....</code></pre></div>\n\n<p>This function expects inputs that have the type <code>list[int]</code>. The typechecker will make sure that every call to <code>avg</code> in typed code match this expectation. But the typechecker will not check any calls to <code>avg</code> that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!</p>\n\n<p>Consequently, untyped code can ask outrageous questions when the program runs:</p>\n\n<pre><code>avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)</code></pre>\n\n<p>We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?</p>\n\n<ul>\n <li>One option is to do nothing. Let the programmer beware that gradual types are unsound at the boundaries to untyped code. With this mindset, types remain cost-free but give zero help for debugging. Many languages follow this approach, including TypeScript and mypy.</li>\n <li>Another option is to enforce type soundness with runtime checks. Now we have reliable types (to some extent), but we also have costs to measure and minimize.</li></ul>\n\n<p>The GTP Benchmarks are a collection of 21 programs designed to test the costs of sound gradual types. Each program comes in two forms, untyped and typed (written in Racket and Typed Racket), with the crucial property that any module-by-module mix of the two forms results in a working program. A benchmark with <code>N</code> modules generates <code>2^N</code> partially-typed programs that sample the space of gradual possibilities:</p>\n\n<p><img src=\"/img/gtp-lattice.png\" width=\"50%\" /></p>\n\n<p>The table below is a birds-eye view of the benchmarks. It lists their name, purpose, and characteristics: whether they were originally typed (T Init), whether they depend on untyped (U Lib) or typed (T Lib) library code, whether they define generative datatypes (Adapt), and whether they send higher-order function (HOF), polymorphic types (Poly), recursive types (Rec), mutable data-structure types (Mut), immutable data-structure types (Imm), object types (Obj), or class types (Cls) across any untyped boundary:</p>\n\n<p><img src=\"/img/gtp-programs.png\" /></p>\n\n<p>For more details, see <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#g-rep-2023\">the paper</a>.</p>")) ((? . 8) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 8) 1721944395 (p+ #"/Users/ashton/Sync/repos/utahplt.github.io/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2023-06-26T01:11:11") #f (? . 7) () (? . 1) #f (? . 1))))
		((3) 0 () 9 ((p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-26-type-tailoring.md" . unix) (u . "") (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-04-21-forge.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-07-07-ltlf.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-06-28-gtp-benchmarks.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2024-02-02-luau-telemetry.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-06-26-flowfpx-juliacon.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-10-31-conceptual-mutant-testing.md" . unix) (p+ #"/Users/ben/code/uu/blog/_src/posts/2023-09-19-generating-programs-trivially.md" . unix)) () (h ! (equal) ((? . 0) f post (u . "[Evolving Languages Faster with Type Tailoring](https://lambdaland.org/posts/2024-07-15_type_tailoring/)") (? . 0) 1722436704 (p+ #"/Users/ben/code/uu/blog/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html" . unix) (u . "/2024/07/-evolving-languages-faster-with-type-tailoring-https-lambdaland-org-posts-2024-07-15-type-tailoring.html") (u . "2024-07-26T14:07:34") (? . 3) #f () (? . 1) #f (? . 1)) ((? . 2) f post (u . "[Forge: A Tool to Teach Formal Methods](https://blog.brownplt.org/2024/04/21/forge.html)") (? . 2) 1719613724 (p+ #"/Users/ben/code/uu/blog/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html" . unix) (u . "/2024/04/-forge-a-tool-to-teach-formal-methods-https-blog-brownplt-org-2024-04-21-forge-html.html") (u . "2024-04-21T01:11:11") (? . 5) (? . 3) () (? . 1) #f (? . 1)) ((? . 4) f post (u . "GTP Benchmarks for Gradual Typing Performance") (? . 4) 1720879367 (p+ #"/Users/ben/code/uu/blog/2023/06/gtp-benchmarks-for-gradual-typing-performance.html" . unix) (u . "/2023/06/gtp-benchmarks-for-gradual-typing-performance.html") (u . "2023-06-28T17:18:44") (? . 6) (? . 8) (c (u . "by Ben Greenman")) (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>") #t (u . "\n<p>Sound gradual types have runtime costs. The GTP Benchmarks have helped measure these costs since 2014.</p>\n<!-- more-->\n\n<hr />\n\n<p>What on earth is gradual typing performance and why does it matter?</p>\n\n<p>The second question is easy to answer: performance matters because the cost of gradual types can slow a program by several <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#tfgnvf-popl-2016\">orders of magnitude</a>. To answer the first question, we need to step back a bit…</p>\n\n<p>Normally, a type system is an ahead-of-time thing. Programs must typecheck before they can run. Afterwards, types can disappear. Compiled code can safely run full-throttle and assume that everything in its world behaves in a well-typed way.</p>\n\n<p>Gradual typing leads to an entirely different situation. It allows typed and untyped code to live together, which means that part of the codebase might rely on type assumptions that the rest of the codebase does not know about!</p>\n\n<p>Suppose we have a typed function that averages the elements in a list:</p>\n\n<div class=\"brush: python\">\n <pre><code>def avg(nums: list[int]):\n ....</code></pre></div>\n\n<p>This function expects inputs that have the type <code>list[int]</code>. The typechecker will make sure that every call to <code>avg</code> in typed code match this expectation. But the typechecker will not check any calls to <code>avg</code> that appear in untyped code. How could it? Untyped code is, by definition, untyped and un-checked!</p>\n\n<p>Consequently, untyped code can ask outrageous questions when the program runs:</p>\n\n<pre><code>avg(\"hello\")\navg([[1, 7], \"X\", 0])\navg(avg)</code></pre>\n\n<p>We clearly have a problem. Typed code might contain elegant data descriptions that untyped code does not know about. What to do?</p>\n\n<ul>\n <li>One option is to do nothing. Let the programmer beware that gradual types are unsound at the boundaries to untyped code. With this mindset, types remain cost-free but give zero help for debugging. Many languages follow this approach, including TypeScript and mypy.</li>\n <li>Another option is to enforce type soundness with runtime checks. Now we have reliable types (to some extent), but we also have costs to measure and minimize.</li></ul>\n\n<p>The GTP Benchmarks are a collection of 21 programs designed to test the costs of sound gradual types. Each program comes in two forms, untyped and typed (written in Racket and Typed Racket), with the crucial property that any module-by-module mix of the two forms results in a working program. A benchmark with <code>N</code> modules generates <code>2^N</code> partially-typed programs that sample the space of gradual possibilities:</p>\n\n<p><img src=\"/img/gtp-lattice.png\" width=\"50%\" /></p>\n\n<p>The table below is a birds-eye view of the benchmarks. It lists their name, purpose, and characteristics: whether they were originally typed (T Init), whether they depend on untyped (U Lib) or typed (T Lib) library code, whether they define generative datatypes (Adapt), and whether they send higher-order function (HOF), polymorphic types (Poly), recursive types (Rec), mutable data-structure types (Mut), immutable data-structure types (Imm), object types (Obj), or class types (Cls) across any untyped boundary:</p>\n\n<p><img src=\"/img/gtp-programs.png\" /></p>\n\n<p>For more details, see <a href=\"https://users.cs.utah.edu/~blg/publications/publications.html#g-rep-2023\">the paper</a>.</p>")) ((? . 5) f post (u . "[Privacy-Respecting Type Error Telemetry at Scale](https://blog.brownplt.org/2024/02/02/privacy-telemetry.html)") (? . 5) 1719613751 (p+ #"/Users/ben/code/uu/blog/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html" . unix) (u . "/2024/02/-privacy-respecting-type-error-telemetry-at-scale-https-blog-brownplt-org-2024-02-02-privacy-telemetry-html.html") (u . "2024-02-02T01:11:11") (? . 7) (? . 2) () (? . 1) #f (? . 1)) ((? . 6) f post (u . "[FlowFPX: Nimble Tools for Debugging Floating-Point Exceptions](https://lambdaland.org/#flowfpx-nimble-tools-for-debugging-floating-point-exceptions--juliacon-2023)") (? . 6) 1720882180 (p+ #"/Users/ben/code/uu/blog/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html" . unix) (u . "/2023/06/-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-https-lambdaland-org-flowfpx-nimble-tools-for-debugging-floating-point-exceptions-juliacon-2023.html") (u . "2023-06-26T01:11:11") #f (? . 4) () (? . 1) #f (? . 1)) ((? . 3) f post (u . "[Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic](https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html)") (? . 3) 1720817329 (p+ #"/Users/ben/code/uu/blog/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html" . unix) (u . "/2024/07/-misconceptions-in-finite-trace-and-infinite-trace-linear-temporal-logic-https-blog-brownplt-org-2024-07-07-little-tricky-logics-2-html.html") (u . "2024-07-07T01:11:11") (? . 2) (? . 0) () (? . 1) #f (? . 1)) ((? . 7) f post (u . "[Conceptual Mutation Testing](https://blog.brownplt.org/2023/10/31/conceptual-mutation-testing.html)") (? . 7) 1719613783 (p+ #"/Users/ben/code/uu/blog/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html" . unix) (u . "/2023/10/-conceptual-mutation-testing-https-blog-brownplt-org-2023-10-31-conceptual-mutation-testing-html.html") (u . "2023-10-31T01:11:11") (? . 8) (? . 5) () (? . 1) #f (? . 1)) ((? . 8) f post (u . "[Generating Programs Trivially: Student Use of Large Language Models](https://blog.brownplt.org/2023/09/19/generating-programs-trivially.html)") (? . 8) 1719613991 (p+ #"/Users/ben/code/uu/blog/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html" . unix) (u . "/2023/09/-generating-programs-trivially-student-use-of-large-language-models-https-blog-brownplt-org-2023-09-19-generating-programs-trivially-html.html") (u . "2023-09-19T01:11:11") (? . 4) (? . 7) () (? . 1) #f (? . 1))))