Hacker News Reader

Comment by nickpsecurity | Hacker News Reader

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/pres...

Among other interesting features. I recommend reading old one then new one.

View on HN

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

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.

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.

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! :)

Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.

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.

Reply on news.ycombinator.com