# \#agda

**URL:** https://discuss.ocaml.org/tag/agda/262.md

[Latest](https://discuss.ocaml.org/latest.md) · [Categories](https://discuss.ocaml.org/categories.md) · [Tags](https://discuss.ocaml.org/tags.md)

---

## [Experimental OCaml backend for Agda](https://discuss.ocaml.org/t/experimental-ocaml-backend-for-agda/2836)

<div class="topic-metadata">

**Author:** [@xekoukou](https://discuss.ocaml.org/u/xekoukou)\
**Replies:** 0\
**Last updated:** [November 6, 2018, 12:10pm UTC](https://discuss.ocaml.org/t/experimental-ocaml-backend-for-agda/2836 "2018-11-06T12:10:37Z")

</div>

agda-ocaml is an experimental backend for Agda, that uses the OCaml runtime. Even though it is still experimental, one of the benefits it might have to OCaml programmers is that it allows programmers to effortlessly sw…

---

## [Which language to use for general programming with dependent types?](https://discuss.ocaml.org/t/which-language-to-use-for-general-programming-with-dependent-types/2494)

<div class="topic-metadata">

**Author:** [@UnixJunkie](https://discuss.ocaml.org/u/UnixJunkie)\
**Replies:** 22\
**Last updated:** [September 7, 2018, 1:28am UTC](https://discuss.ocaml.org/t/which-language-to-use-for-general-programming-with-dependent-types/2494 "2018-09-07T01:28:44Z")

</div>

Hello, Let’s say I want to do system/backend programming using a language with dependent types (just to give it a try). Which one of those would be the best considering agility of the programmer (I want to do softwar…