3 ms·

It does exist and it's called Racket [1] and language-oriented programming. You can write prolog-like languages [2], or Haskell-like [3], or even C-like languag

It does exist and it's called Racket [1] and language-oriented programming. You can write prolog-like languages [2], or Haskell-like [3], or even C-like languages [4]. You can even write BNF directly [5] and you can /call/ these constructs across different languages. Racket makes it /easy/ to play with semantics and syntax. You can feasibly write a language in an afternoon, to solve 1 specific problem. [1] https://racket-lang.org/ https://racket-lang.org/ [2] https://docs.racket-lang.org/datalog/datalog.html?q=datalog https://docs.racket-lang.org/datalog/datalog.html?q=datalog [3] https://github.com/lexi-lambda/hackett https://github.com/lexi-lambda/hackett [4] https://docs.racket-lang.org/profj/ https://docs.racket-lang.org/profj/ [5] https://beautifulracket.com/appendix/why-lop-why-racket.html https://beautifulracket.com/appendix/why-lop-why-racket.html

dgb23 6y ago
I used Racket at some point alongside SICP ~10y ago. I always considered it being a pure educational/experimental/research language. While this is likely a primary focus of Racket, it seems to be there is a ton to be gained from diving deeper into it, so thank you for these resources.
nextos 6y ago
In my opinion, a promising avenue for programming would be DSLs with restricted semantics + SAT/SMT solving to deliver lightweight formal methods. So, instead of programming in Turing-complete languages, one creates many specialized DSLs with just enough expressiveness. And, in parallel, some automated formal methods. The combination of a DSL and SAT/SMT makes this feasible, which contrasts with automated theorem proving on Turing-complete languages. Racket seems like a good platform to do this.
- ywei3410 6y ago
  Yes! There is some work being done in this space already; by the incredible people at North-Eastern. One of the more interesting parts of this problem is what you do at the /boundaries/ of the different languages with differing semantics such that you don't accidentally introduce bad lemmas. There are a few published papers which study the boundary between dynamic and static type-systems, but the hope was to extend it into gradual-typing between different type-systems .
  - nextos 6y ago
    I think I know some of these papers, but could you please point me to some of the references you have mentioned?
    - ywei3410 6y ago
      Of course — this paper talks about the mechanism which Racket explores to keep the boundary safe [1]. This paper [2] elaborates on some of the performance challenges. 'Shallow typing' by Ben Greenman et al. is available only by video [3] and slideshow form [4]. Finally, there's a really interesting paper which came out this year which uses a verifier to remove the some of the runtime cost [5] of sound gradual typing. [1] https://www.cs.utah.edu/plt/publications/oopsla12-stff.pdf https://www.cs.utah.edu/plt/publications/oopsla12-stff.pdf [2] https://www2.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf https://www2.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf [3] https://www.youtube.com/watch?v=A4AA8nweYAg https://www.youtube.com/watch?v=A4AA8nweYAg [4] https://www.ccs.neu.edu/~types/resources/talks/g-rcon-2020.pdf https://www.ccs.neu.edu/~types/resources/talks/g-rcon-2020.p... [5] https://arxiv.org/abs/2007.12630 https://arxiv.org/abs/2007.12630
      - nextos 6y ago
        Thank you so much!

dgb23 6y ago

I used Racket at some point alongside SICP ~10y ago. I always considered it being a pure educational/experimental/research language. While this is likely a primary focus of Racket, it seems to be there is a ton to be gained from diving deeper into it, so thank you for these resources.

nextos 6y ago

In my opinion, a promising avenue for programming would be DSLs with restricted semantics + SAT/SMT solving to deliver lightweight formal methods. So, instead of programming in Turing-complete languages, one creates many specialized DSLs with just enough expressiveness. And, in parallel, some automated formal methods. The combination of a DSL and SAT/SMT makes this feasible, which contrasts with automated theorem proving on Turing-complete languages. Racket seems like a good platform to do this.

ywei3410 6y ago
Yes! There is some work being done in this space already; by the incredible people at North-Eastern. One of the more interesting parts of this problem is what you do at the /boundaries/ of the different languages with differing semantics such that you don't accidentally introduce bad lemmas. There are a few published papers which study the boundary between dynamic and static type-systems, but the hope was to extend it into gradual-typing between different type-systems .
- nextos 6y ago
  I think I know some of these papers, but could you please point me to some of the references you have mentioned?
  - ywei3410 6y ago
    Of course — this paper talks about the mechanism which Racket explores to keep the boundary safe [1]. This paper [2] elaborates on some of the performance challenges. 'Shallow typing' by Ben Greenman et al. is available only by video [3] and slideshow form [4]. Finally, there's a really interesting paper which came out this year which uses a verifier to remove the some of the runtime cost [5] of sound gradual typing. [1] https://www.cs.utah.edu/plt/publications/oopsla12-stff.pdf https://www.cs.utah.edu/plt/publications/oopsla12-stff.pdf [2] https://www2.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf https://www2.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf [3] https://www.youtube.com/watch?v=A4AA8nweYAg https://www.youtube.com/watch?v=A4AA8nweYAg [4] https://www.ccs.neu.edu/~types/resources/talks/g-rcon-2020.pdf https://www.ccs.neu.edu/~types/resources/talks/g-rcon-2020.p... [5] https://arxiv.org/abs/2007.12630 https://arxiv.org/abs/2007.12630
    - nextos 6y ago
      Thank you so much!