I like Math, will I enjoy programming too?

• Idris2

  1 54 0.0 Idris

  A purely functional programming language with first class types (by edwinb)

Finally, if you are interested in actually writing code to do things, then you may want to check out Idris (and possibly the next generation built from lessons learned from it but still very much in development, Idris 2) because this language was designed from the ground up to be a practical tool in which to write programs while still being based fundamentally on dependent types and thus being very proof-centric, unlike Coq and Agda which are more specialized in being programming languages in which to express mathematics.

• CPython

  1,320 59,954 10.0 Python

  The Python programming language

  

Of course, if you just want a programming language that is easy to learn and even more widely used but doesn't have a powerful type system because when push come to shove you don't actually care that much whether the code you've just written is correct or not, and in particular you won't mind if half-way through completing some long task your code crashes because you misspelled a variable name when making a change that you hadn't tested carefully enough because it seemed to be obviously fine at the time, there is always Python...

• InfluxDB

  www.influxdata.com featured

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• coq

  87 4,632 10.0 OCaml

  Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

  

One of the oldest and most famous ones I am aware of is Coq (for Chicken, if you were wondering; it's a French thing to name programming languages after animals). In particular I recommend this free online book as an introduction to using Coq to blend programming and proofs.

Suggest a related project