3 ms·
I think there are languages and tools that mathematically minded programmers will find accessible enough and useful to aid them in their thinking. Dependently-t
by agentultra 7y ago
I think there are languages and tools that mathematically minded programmers will find accessible enough and useful to aid them in their thinking. Dependently-typed programming languages such as Lean [0] and Agda [1] are both expressive enough to search for proofs to theorems and practical enough to execute programs.
And in the design space when we're thinking about problems of concurrency or liveness there are great tools like TLA+ that take a pure mathematical model and automate the checking that it satisfies our expectations. [2]
It's not all figures and drawings these days! I see maths and engineering integrating more closely in the future.
[0] https://leanprover.github.io/ https://leanprover.github.io/
[1] https://github.com/agda/agda https://github.com/agda/agda
[2] https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html