Front Page
What is this?
An attempt at organizing my thoughts about programming languages and what I need from them. This is currently composed of three parts:
- A list of languages to analyze.
- Techniques used by those languages in order to improve expressiveness and verifiability.
- A list of challenges meant to tease out the ability of these languages to solve tricky issues.
The end goal is to identify a language (existing, or a hypothetical mixture of approaches pioneered elsewhere), which can:
- Minimize accidental complexity, both up-front and as a consequence of continuously shifting requirements.
- Allow for gradual correctness, where not just new requirements, but new kinds of requirements (including those not anticipated by the original author or the language designer) can be added to existing software, with the existing codebase being brought into compliance with them over time.
Languages
- Ada
- Agda
- Arend
- ATS
- Coq
- Dafny
- Eff
- Eiffel
- Epigram
- Idris
- Isabelle
- Lisp Family
- Mercury
- Pharo Smalltalk
- Prolog
- Shen
- Ur
