gabby

@basile-henry: I think you can still do this while hosting the code on GitHub. All you have to do is to create a proxy that sits in front of the...

There was a relevant discussion on this on Discourse: https://discourse.dhall-lang.org/t/working-with-binary-form-directly-in-expressions/182 In addition to the idea of using the `Accept` header to specify the content type for HTTP(S) imports, @philandstuff also...

@basile-henry: Yeah, I think this is a good idea. My only suggestion is to make the strict behavior the default, with a flag to opt out and recover the old...

@basile-henry: Yeah, I meant to say just for the modification commands like `dhall {format,freeze,lint}`

@basile-henry: Another option might be to change `dhall-docs` to permit those comments. It might actually be a feature to support multiple block comments for documenting something and merging them in...

@SupraSummus: I believe the closest thing to what you have in mind is "program extraction", meaning that the implementation is written in a programming language designed for program extraction (typically...

Actually, from some quick searching it looks like there might be a way to extract Python code from Coq: http://coqcots.gforge.inria.fr/coq8.4pl3-python/

The main advantage of using program extraction over code generation is that the specification is type-checked (a.k.a. certified programming) and you don't have to reinvent a specification language for the...

@indolering: I believe we need something else in addition to WebAssembly interface types. The interface types do support some declarative transformations, but we essentially need a way to encode arbitrary...

Yeah, I think this is a good idea I want to note that this is somewhat similar to another request for providing built-in support for dates and times: https://github.com/dhall-lang/dhall-lang/issues/80 but...