News for hackers. Stuff that matters.

A comment on Show HN: Dependently typed language for proofs that you can implement in one day. Parent comment

Re:Show HN: Dependently typed language for proofs that you c... by lapinot on Sunday October 03, 2021 @08:51AM (#28736809)
Obviously highly subjective, yet heavy of conventions. Usually the subject comes before the qualification. "counter is an integer", "let counter be an integer" instead of "from the integer take counter".
[ Parent | on HN ]
Re:Show HN: Dependently typed language for proofs that you c... by Zababa on Sunday October 03, 2021 @01:49PM (#28739010)
Programming languages aren't natural languages though, and I don't think they should be forced to look like them.

One thing for the "type before name" camp is that you don't have to use a keyword like "let" or "function" when declaring a function, but on the other hand you're going to introduce a keyword anyways if you add type inference.

[ Parent | on HN ]
Re:Show HN: Dependently typed language for proofs that you c... by dllthomas on Tuesday October 12, 2021 @08:46PM (#28846921)
"We have an integer called x, ..."
[ Parent | on HN ]
Re:Show HN: Dependently typed language for proofs that you c... by DemocracyFTW on Sunday October 03, 2021 @11:39AM (#28738010)
You say "Nixon is a President" but also "President Nixon".
[ Parent | on HN ]