6 ms·

Learn You an Agda (2014)

46 points by deterministic 5y ago

Deutscher 5y ago
The LaTeX isn't rendering on any of my mobile browsers. Anyone else see the same?
- defanor 5y ago
  I do: mathjax is served via HTTP, the website is served via HTTPS, so it's blocked (by desktop FF, at least) as mixed content. *.github.io websites used to be HTTP-only back when it was written, IIRC, but now it's HTTPS-only. Apparently in the desktop FF that blocking can be disabled in the connection information menu, though it still blocks that for me after disabling.
dang 5y ago
Related: Learn you an Agda (2011) - https://news.ycombinator.com/item?id=17324469 https://news.ycombinator.com/item?id=17324469 - June 2018 (8 comments) Learn you an Agda - https://news.ycombinator.com/item?id=9456810 https://news.ycombinator.com/item?id=9456810 - April 2015 (24 comments) Learn You an Agda - https://news.ycombinator.com/item?id=8688070 https://news.ycombinator.com/item?id=8688070 - Dec 2014 (70 comments)
bckr 5y ago
> We can statically eliminate any error scenario from our program Well this sounds great. When do I get a version of this in my day job? (Python, Flask, VSCode, MacOS). I really hope software engineering in 10 years is as cool as it can be... formal verification, fast, readable, portable... All the things!
- lambdasquirrel 5y ago
  I think the problem with the PLT space is that it's not monetizable the same way that e.g. ML is. If you get a Ph.D in ML, you have an easy shot at a high paying industry job. Not so with a Ph.D in PLT. That alone provides some force for research. It's hard getting enough investment in the PLT space because the costs that are borne can't be easily recouped. It's a classic problem with research. And we know how much the world runs around money right now.
  - pjmlp 5y ago
    Nowadays, 30 years ago my AI professors where trying to keep their classes open and stuff like neural networks where optional lectures.
  - oxff 5y ago
    Quick, easy formal verification tools that programmers can use on the spot from the IDE are hard to make for most languages because most languages and their compilers weren't made with such thing in mind. I guess Rust might be heading somewhere interesting with tooling, with tools like Flowistry existing (https://github.com/willcrichton/flowistry https://github.com/willcrichton/flowistry) showing what is possible. It's a plugin that can compute backwards / forwards static slices for you, straight in the IDE as a VSCode plugin. I think you need an external program that runs a full program analysis to do the same in C++.
    - pjmlp 5y ago
      Frama-C and Ada/SPARK are two examples of tooling with IDE support and wide use in high integrity computing domain.
- chriswarbo 5y ago
  > Python Probably never. Python provides very few guarantees about anything; e.g. there's a lot of dynamic dispatch which cannot be resolved ahead-of-time, and it's technically possible to mess with lots of things (e.g. swapping a value's __class__ using a random number generator!)
- deterministic 5y ago
  I think it will happen slowly but steadily. There are now a few commercial companies specialising in writing software that is proven correct. CompCert and seL4 are some examples. And various large companies are using tools like TLA+ to prove complex systems correct. However I think it will always be a specialised area (like embedded systems). With new job titles like “Proof Engineer” or “Verification Engineer”.
- mbrodersen 5y ago
  SPARK/Ada is an example of a language/proof system used for real world software. Especially embedded military systems.
tluyben2 5y ago
Agda is nice and this tutorial is actually pretty great imho. I, for some reason, cannot stand when languages are not self hosting (that's my bug though; i'm not saying it's better or worse in general), so for me Idris 2 won out as dependently typed language I use for some proof work.
- mbrodersen 5y ago
  Idris 2 is a nice alternative to Agda. It seems to be a bit more focused on practical programming.

46 points by deterministic 5y ago

Deutscher 5y ago

The LaTeX isn't rendering on any of my mobile browsers. Anyone else see the same?

defanor 5y ago
I do: mathjax is served via HTTP, the website is served via HTTPS, so it's blocked (by desktop FF, at least) as mixed content. *.github.io websites used to be HTTP-only back when it was written, IIRC, but now it's HTTPS-only. Apparently in the desktop FF that blocking can be disabled in the connection information menu, though it still blocks that for me after disabling.

dang 5y ago

Related: Learn you an Agda (2011) - https://news.ycombinator.com/item?id=17324469 https://news.ycombinator.com/item?id=17324469 - June 2018 (8 comments) Learn you an Agda - https://news.ycombinator.com/item?id=9456810 https://news.ycombinator.com/item?id=9456810 - April 2015 (24 comments) Learn You an Agda - https://news.ycombinator.com/item?id=8688070 https://news.ycombinator.com/item?id=8688070 - Dec 2014 (70 comments)

bckr 5y ago

> We can statically eliminate any error scenario from our program Well this sounds great. When do I get a version of this in my day job? (Python, Flask, VSCode, MacOS). I really hope software engineering in 10 years is as cool as it can be... formal verification, fast, readable, portable... All the things!

lambdasquirrel 5y ago
I think the problem with the PLT space is that it's not monetizable the same way that e.g. ML is. If you get a Ph.D in ML, you have an easy shot at a high paying industry job. Not so with a Ph.D in PLT. That alone provides some force for research. It's hard getting enough investment in the PLT space because the costs that are borne can't be easily recouped. It's a classic problem with research. And we know how much the world runs around money right now.
- pjmlp 5y ago
  Nowadays, 30 years ago my AI professors where trying to keep their classes open and stuff like neural networks where optional lectures.
- oxff 5y ago
  Quick, easy formal verification tools that programmers can use on the spot from the IDE are hard to make for most languages because most languages and their compilers weren't made with such thing in mind. I guess Rust might be heading somewhere interesting with tooling, with tools like Flowistry existing (https://github.com/willcrichton/flowistry https://github.com/willcrichton/flowistry) showing what is possible. It's a plugin that can compute backwards / forwards static slices for you, straight in the IDE as a VSCode plugin. I think you need an external program that runs a full program analysis to do the same in C++.
  - pjmlp 5y ago
    Frama-C and Ada/SPARK are two examples of tooling with IDE support and wide use in high integrity computing domain.
chriswarbo 5y ago
> Python Probably never. Python provides very few guarantees about anything; e.g. there's a lot of dynamic dispatch which cannot be resolved ahead-of-time, and it's technically possible to mess with lots of things (e.g. swapping a value's __class__ using a random number generator!)
deterministic 5y ago
I think it will happen slowly but steadily. There are now a few commercial companies specialising in writing software that is proven correct. CompCert and seL4 are some examples. And various large companies are using tools like TLA+ to prove complex systems correct. However I think it will always be a specialised area (like embedded systems). With new job titles like “Proof Engineer” or “Verification Engineer”.
mbrodersen 5y ago
SPARK/Ada is an example of a language/proof system used for real world software. Especially embedded military systems.

tluyben2 5y ago

Agda is nice and this tutorial is actually pretty great imho. I, for some reason, cannot stand when languages are not self hosting (that's my bug though; i'm not saying it's better or worse in general), so for me Idris 2 won out as dependently typed language I use for some proof work.

mbrodersen 5y ago
Idris 2 is a nice alternative to Agda. It seems to be a bit more focused on practical programming.