3 ms·

It would take a lot of talent and time to use. It's why I usually push Design-by-Contract and/or runtime checks/tests. Far as new languages, you might find Noet

It would take a lot of talent and time to use. It's why I usually push Design-by-Contract and/or runtime checks/tests. Far as new languages, you might find Noether interesting in how it is built in layers that let one trade verification difficulty vs expressiveness as desired. https://github.com/noether-lang/noether/tree/master/doc/presentations https://github.com/noether-lang/noether/tree/master/doc/pres... Among other interesting features. I recommend reading old one then new one.

adamnemecek 9y ago
I would imagine an idris derivative isnt all that much easier to write when compared with writing coq.
- nickpsecurity 9y ago
  Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work. Plus, I thought you'd enjoy the language presentation as extra benefit.
  - willtim 9y ago
    Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.
  - unboxed_type 9y ago
    I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)
- mietek 9y ago
  Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.
- johnbender 9y ago
  I agree. I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer. As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to good documentation and other resources.

adamnemecek 9y ago

I would imagine an idris derivative isnt all that much easier to write when compared with writing coq.

nickpsecurity 9y ago
Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work. Plus, I thought you'd enjoy the language presentation as extra benefit.
- willtim 9y ago
  Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.
- unboxed_type 9y ago
  I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)
mietek 9y ago
Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.
johnbender 9y ago
I agree. I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer. As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to good documentation and other resources.