From c35e37d9a0298a54c6205617c43a35cc7706a37a Mon Sep 17 00:00:00 2001 From: ben Date: Sat, 5 Mar 2016 13:43:04 -0500 Subject: [PATCH] [icfp] put 'correctness' inside 'solution' --- icfp-2016/correctness.scrbl | 14 -------------- icfp-2016/implementation.scrbl | 22 ++++++++++++++++++++++ 2 files changed, 22 insertions(+), 14 deletions(-) delete mode 100644 icfp-2016/correctness.scrbl diff --git a/icfp-2016/correctness.scrbl b/icfp-2016/correctness.scrbl deleted file mode 100644 index 48b737a..0000000 --- a/icfp-2016/correctness.scrbl +++ /dev/null @@ -1,14 +0,0 @@ -@title{Correctness} - -Our implementation of @racket[format] in @todo{figure-ref} exhibits a few desirable properties. -@itemlist[ - @item{} -] - -Generally speaking these properties are the ``right'' way to judge if a transformation is correct. - - - -Open question: can we design a restricted macro language where every transformation - is statically checked to ensure termination and correctness. - diff --git a/icfp-2016/implementation.scrbl b/icfp-2016/implementation.scrbl index 0248d59..f8b7683 100644 --- a/icfp-2016/implementation.scrbl +++ b/icfp-2016/implementation.scrbl @@ -13,3 +13,25 @@ @; We don't re-implement format or regexp, @; but we do implement + and some vector operations, to go faster + + + + + +@section{Correctness} + +Our implementation of @racket[format] in @todo{figure-ref} exhibits a few desirable properties. +@itemlist[ + @item{} +] + +Generally speaking these properties are the ``right'' way to judge if a transformation is correct. + + + +Open question: can we design a restricted macro language where every transformation + is statically checked to ensure termination and correctness. + +We have argued that our macros help typed programming, but they did so only + by going outside the law of the type checker. +